Theorem axnulALT

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , sp , and ax-rep . To check this, replace sp with the obsolete axiom ax-c5 in the proof of axnulALT and type the Metamath program "MM> SHOW TRACE__BACK axnulALT / AXIOMS" command. (Contributed by Jeff Hoffman, 3-Feb-2008) (Proof shortened by Mario Carneiro, 17-Nov-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axnulALT	|- E. x A. y -. y e. x

Proof

Step	Hyp	Ref	Expression
1		ax-rep	|- ( A. w E. x A. y ( A. x F. -> y = x ) -> E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
2		sp	|- ( A. x -. A. y ( A. x F. -> y = x ) -> -. A. y ( A. x F. -> y = x ) )
3	2	con2i	|- ( A. y ( A. x F. -> y = x ) -> -. A. x -. A. y ( A. x F. -> y = x ) )
4		df-ex	|- ( E. x A. y ( A. x F. -> y = x ) <-> -. A. x -. A. y ( A. x F. -> y = x ) )
5	3 4	sylibr	|- ( A. y ( A. x F. -> y = x ) -> E. x A. y ( A. x F. -> y = x ) )
6		fal	|- -. F.
7		sp	|- ( A. x F. -> F. )
8	6 7	mto	|- -. A. x F.
9	8	pm2.21i	|- ( A. x F. -> y = x )
10	5 9	mpg	|- E. x A. y ( A. x F. -> y = x )
11	1 10	mpg	|- E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) )
12	8	intnan	|- -. ( w e. z /\ A. x F. )
13	12	nex	|- -. E. w ( w e. z /\ A. x F. )
14	13	nbn	|- ( -. y e. x <-> ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
15	14	albii	|- ( A. y -. y e. x <-> A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
16	15	exbii	|- ( E. x A. y -. y e. x <-> E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
17	11 16	mpbir	|- E. x A. y -. y e. x