Apply df_rmo__df_rab__df_v__df_cdeq__df_sbc__df_csb__df_dif__df_un__df_in__df_ss__df_pss__df_symdif__df_nul__df_if__df_pw__df_sn__df_pr__df_tp with
∀ x0 x1 x2 : ι → ο . wceq (ctp x0 x1 x2) (cun (cpr x0 x1) (csn x2)).
Assume H0:
∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wrmo (λ x2 . x0 x2) (λ x2 . x1 x2)) (wmo (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))).
Assume H1:
∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wceq (crab (λ x2 . x0 x2) (λ x2 . x1 x2)) (cab (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))).
Assume H3:
∀ x0 : ο . ∀ x1 x2 . wb (wcdeq x0 x1 x2) (wceq (cv x1) (cv x2) ⟶ x0).
Assume H4:
∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 . wb (wsbc (λ x3 . x0 x3) (x1 x2)) (wcel (x1 x2) (cab (λ x3 . x0 x3))).
Assume H5:
∀ x0 x1 : ι → ι → ο . ∀ x2 . wceq (csb (x0 x2) (λ x3 . x1 x3)) (cab (λ x3 . wsbc (λ x4 . wcel (cv x3) (x1 x4)) (x0 x2))).
Assume H9:
∀ x0 x1 : ι → ο . wb (wss x0 x1) (wceq (cin x0 x1) x0).
Assume H10:
∀ x0 x1 : ι → ο . wb (wpss x0 x1) (wa (wss x0 x1) (wne x0 x1)).