Metamath Proof Explorer

Theorem zfinf

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

Ref Expression
Assertion zfinf ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 ax-inf ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)\right)\right)$
2 elequ1 ${⊢}{w}={y}\to \left({w}\in {x}↔{y}\in {x}\right)$
3 elequ1 ${⊢}{w}={y}\to \left({w}\in {z}↔{y}\in {z}\right)$
4 3 anbi1d ${⊢}{w}={y}\to \left(\left({w}\in {z}\wedge {z}\in {x}\right)↔\left({y}\in {z}\wedge {z}\in {x}\right)\right)$
5 4 exbidv ${⊢}{w}={y}\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)$
6 2 5 imbi12d ${⊢}{w}={y}\to \left(\left({w}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)\right)↔\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)\right)$
7 6 cbvalvw ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)$
8 7 anbi2i ${⊢}\left({y}\in {x}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)\right)\right)↔\left({y}\in {x}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)\right)$
9 8 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}\in {x}\right)\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)\right)$
10 1 9 mpbi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\wedge {z}\in {x}\right)\right)\right)$