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