Metamath Proof Explorer

Theorem zfun

Description: Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003) Use ax-un instead. (New usage is discouraged.)

Ref Expression
Assertion zfun ⊢∃x∀y∃xy∈x∧x∈z→y∈x

Proof

Step Hyp Ref Expression
1 ax-un ⊢∃x∀y∃wy∈w∧w∈z→y∈x
2 elequ2 ⊢w=x→y∈w↔y∈x
3 elequ1 ⊢w=x→w∈z↔x∈z
4 2 3 anbi12d ⊢w=x→y∈w∧w∈z↔y∈x∧x∈z
5 4 cbvexvw ⊢∃wy∈w∧w∈z↔∃xy∈x∧x∈z
6 5 imbi1i ⊢∃wy∈w∧w∈z→y∈x↔∃xy∈x∧x∈z→y∈x
7 6 albii ⊢∀y∃wy∈w∧w∈z→y∈x↔∀y∃xy∈x∧x∈z→y∈x
8 7 exbii ⊢∃x∀y∃wy∈w∧w∈z→y∈x↔∃x∀y∃xy∈x∧x∈z→y∈x
9 1 8 mpbi ⊢∃x∀y∃xy∈x∧x∈z→y∈x