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	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )

Proof

Step	Hyp	Ref	Expression
1		axunnd	|- E. y A. z ( E. y ( z e. y /\ y e. x ) -> z e. y )
2		elequ2	|- ( w = y -> ( z e. w <-> z e. y ) )
3		elequ1	|- ( w = y -> ( w e. x <-> y e. x ) )
4	2 3	anbi12d	|- ( w = y -> ( ( z e. w /\ w e. x ) <-> ( z e. y /\ y e. x ) ) )
5	4	cbvexvw	|- ( E. w ( z e. w /\ w e. x ) <-> E. y ( z e. y /\ y e. x ) )
6	5	imbi1i	|- ( ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> ( E. y ( z e. y /\ y e. x ) -> z e. y ) )
7	6	albii	|- ( A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> A. z ( E. y ( z e. y /\ y e. x ) -> z e. y ) )
8	7	exbii	|- ( E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> E. y A. z ( E. y ( z e. y /\ y e. x ) -> z e. y ) )
9	1 8	mpbir	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )