Theorem axnulALT 4524

Description: Alternate proof of axnul 4525, proved directly from ax-rep 4508 using none of the equality axioms ax-7 1859 through ax-c14 32527 provided we accept sp 1957 as an axiom. Replace sp 1957 with the obsolete ax-c5 32519 to see this in 'show trace_back'. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, y

Proof of Theorem axnulALT

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-rep 4508	. . 3 |- ( 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 1957	. . . . . 6 |- ( A. x -. A. y ( A. x F. -> y = x ) -> -. A. y ( A. x F. -> y = x ) )
3	2	con2i 124	. . . . 5 |- ( A. y ( A. x F. -> y = x ) -> -. A. x -. A. y ( A. x F. -> y = x ) )
4		df-ex 1672	. . . . 5 |- ( E. x A. y ( A. x F. -> y = x ) <-> -. A. x -. A. y ( A. x F. -> y = x ) )
5	3, 4	sylibr 217	. . . 4 |- ( A. y ( A. x F. -> y = x ) -> E. x A. y ( A. x F. -> y = x ) )
6		fal 1459	. . . . . 6 |- -. F.
7		sp 1957	. . . . . 6 |- ( A. x F. -> F. )
8	6, 7	mto 181	. . . . 5 |- -. A. x F.
9	8	pm2.21i 136	. . . 4 |- ( A. x F. -> y = x )
10	5, 9	mpg 1679	. . 3 |- E. x A. y ( A. x F. -> y = x )
11	1, 10	mpg 1679	. 2 |- E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) )
12	8	intnan 928	. . . . . 6 |- -. ( w e. z /\ A. x F. )
13	12	nex 1686	. . . . 5 |- -. E. w ( w e. z /\ A. x F. )
14	13	nbn 354	. . . 4 |- ( -. y e. x <-> ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
15	14	albii 1699	. . 3 |- ( A. y -. y e. x <-> A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
16	15	exbii 1726	. 2 |- ( 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 214	1 |- E. x A. y -. y e. x

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   A.wal 1450   = wceq 1452   F. wfal 1457   E.wex 1671   e. wcel 1904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-rep 4508

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-fal 1458  df-ex 1672

This theorem is referenced by: (None)