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

Metamath Proof Explorer

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