MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12o Unicode version

Theorem ax12o 1976
Description: Derive set.mm's original ax-12o 2192 from the shorter ax-12 1946. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Revised by Wolf Lammen, 30-Jan-2018.)
Assertion
Ref Expression
ax12o  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )

Proof of Theorem ax12o
Dummy variables  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax12v 1947 . . 3  |-  ( -.  z  =  x  -> 
( x  =  w  ->  A. z  x  =  w ) )
2 ax12v 1947 . . 3  |-  ( -.  z  =  x  -> 
( x  =  v  ->  A. z  x  =  v ) )
31, 2ax12olem3 1974 . 2  |-  ( -. 
A. z  z  =  x  ->  F/ z  x  =  w )
4 ax12v 1947 . . 3  |-  ( -.  z  =  y  -> 
( y  =  w  ->  A. z  y  =  w ) )
5 ax12v 1947 . . 3  |-  ( -.  z  =  y  -> 
( y  =  v  ->  A. z  y  =  v ) )
64, 5ax12olem3 1974 . 2  |-  ( -. 
A. z  z  =  y  ->  F/ z 
y  =  w )
73, 6ax12olem4 1975 1  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546
This theorem is referenced by:  ax12  1985  ax12OLD  1986  dvelimvOLD  1994  hbae  2005  nfeqf  2014  dvelimhOLD  2016  dvelimf  2050  dvelimALT  2183  ax11eq  2243  ax11indalem  2247  axi12  2383  axbnd  2384  axext4dist  25371
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator