Metamath Proof Explorer


Theorem zfcndun

Description: Axiom of Union ax-un , reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion zfcndun y z w z w w x z y

Proof

Step Hyp Ref Expression
1 axunnd y z y z y y x z y
2 elequ2 w = y z w z y
3 elequ1 w = y w x y x
4 2 3 anbi12d w = y z w w x z y y x
5 4 cbvexvw w z w w x y z y y x
6 5 imbi1i w z w w x z y y z y y x z y
7 6 albii z w z w w x z y z y z y y x z y
8 7 exbii y z w z w w x z y y z y z y y x z y
9 1 8 mpbir y z w z w w x z y