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