This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 )