Theorem axnulALT 4580

Description: Alternate proof of axnul 4581, proved directly from ax-rep 4564 using none of the equality axioms ax-7 1739 through ax-c14 2215 provided we accept sp 1808 as an axiom. Replace sp 1808 with the obsolete ax-c5 2207 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 4564	. . 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 1808	. . . . . 6 |- ( A. x -. A. y ( A. x F. -> y = x ) -> -. A. y ( A. x F. -> y = x ) )
3	2	con2i 120	. . . . 5 |- ( A. y ( A. x F. -> y = x ) -> -. A. x -. A. y ( A. x F. -> y = x ) )
4		df-ex 1597	. . . . 5 |- ( E. x A. y ( A. x F. -> y = x ) <-> -. A. x -. A. y ( A. x F. -> y = x ) )
5	3, 4	sylibr 212	. . . 4 |- ( A. y ( A. x F. -> y = x ) -> E. x A. y ( A. x F. -> y = x ) )
6		fal 1386	. . . . . 6 |- -. F.
7		sp 1808	. . . . . 6 |- ( A. x F. -> F. )
8	6, 7	mto 176	. . . . 5 |- -. A. x F.
9	8	pm2.21i 131	. . . 4 |- ( A. x F. -> y = x )
10	5, 9	mpg 1603	. . 3 |- E. x A. y ( A. x F. -> y = x )
11	1, 10	mpg 1603	. 2 |- E. x A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) )
12	8	intnan 912	. . . . . 6 |- -. ( w e. z /\ A. x F. )
13	12	nex 1610	. . . . 5 |- -. E. w ( w e. z /\ A. x F. )
14	13	nbn 347	. . . 4 |- ( -. y e. x <-> ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
15	14	albii 1620	. . 3 |- ( A. y -. y e. x <-> A. y ( y e. x <-> E. w ( w e. z /\ A. x F. ) ) )
16	15	exbii 1644	. 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 209	1 |- E. x A. y -. y e. x

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1377   = wceq 1379   F. wfal 1384   E.wex 1596   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-rep 4564

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-fal 1385  df-ex 1597

This theorem is referenced by: (None)