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

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

Proof

Step Hyp Ref Expression
1 ax-inf 
 |-  E. x ( y e. x /\ A. w ( w e. x -> E. z ( w e. z /\ z e. x ) ) )
2 elequ1 
 |-  ( w = y -> ( w e. x <-> y e. x ) )
3 elequ1 
 |-  ( w = y -> ( w e. z <-> y e. z ) )
4 3 anbi1d 
 |-  ( w = y -> ( ( w e. z /\ z e. x ) <-> ( y e. z /\ z e. x ) ) )
5 4 exbidv 
 |-  ( w = y -> ( E. z ( w e. z /\ z e. x ) <-> E. z ( y e. z /\ z e. x ) ) )
6 2 5 imbi12d 
 |-  ( w = y -> ( ( w e. x -> E. z ( w e. z /\ z e. x ) ) <-> ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
7 6 cbvalvw 
 |-  ( A. w ( w e. x -> E. z ( w e. z /\ z e. x ) ) <-> A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
8 7 anbi2i 
 |-  ( ( y e. x /\ A. w ( w e. x -> E. z ( w e. z /\ z e. x ) ) ) <-> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
9 8 exbii 
 |-  ( E. x ( y e. x /\ A. w ( w e. x -> E. z ( w e. z /\ z e. x ) ) ) <-> E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
10 1 9 mpbi 
 |-  E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )