Apply df_op__df_ot__df_uni__df_int__df_iun__df_iin__df_disj__df_br__df_opab__df_opab_b__df_mpt__df_tr__ax_rep__ax_pow__df_id__df_eprel__df_po__df_so with
∀ x0 x1 : ι → ι → ο . wceq (cmpt (λ x2 . x0 x2) (λ x2 . x1 x2)) (copab (λ x2 x3 . wa (wcel (cv x2) (x0 x2)) (wceq (cv x3) (x1 x2)))).
Assume H1:
∀ x0 x1 x2 : ι → ο . wceq (cotp x0 x1 x2) (cop (cop x0 x1) x2).
Assume H4:
∀ x0 x1 : ι → ι → ο . wceq (ciun (λ x2 . x0 x2) (λ x2 . x1 x2)) (cab (λ x2 . wrex (λ x3 . wcel (cv x2) (x1 x3)) (λ x3 . x0 x3))).
Assume H5:
∀ x0 x1 : ι → ι → ο . wceq (ciin (λ x2 . x0 x2) (λ x2 . x1 x2)) (cab (λ x2 . wral (λ x3 . wcel (cv x2) (x1 x3)) (λ x3 . x0 x3))).
Assume H6:
∀ x0 x1 : ι → ι → ο . wb (wdisj (λ x2 . x0 x2) (λ x2 . x1 x2)) (∀ x2 . wrmo (λ x3 . wcel (cv x2) (x1 x3)) (λ x3 . x0 x3)).
Assume H7:
∀ x0 x1 x2 : ι → ο . wb (wbr x0 x1 x2) (wcel (cop x0 x1) x2).
Assume H10:
∀ x0 x1 : ι → ι → ο . wceq (cmpt (λ x2 . x0 x2) (λ x2 . x1 x2)) (copab (λ x2 x3 . wa (wcel (cv x2) (x0 x2)) (wceq (cv x3) (x1 x2)))).
Assume H12:
∀ x0 : ι → ι → ι → ο . ∀ x1 . ... ⟶ wex (λ x2 . ...).