Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax12wK Unicode version

Theorem ax12wK 27930
Description: Weak version (principal instance) of ax-12 1633 not involving bundling. Uses only Tarski's FOL axiom schemes (see description for equidK 27889). The proof is trivial but is included to complete the set ax6wK 27919, ax7wK 27922, and ax11wK 27927. See the description in the comment of equidK 27889. (Contributed by NM, 10-Apr-2017.)
Assertion
Ref Expression
ax12wK  |-  ( -.  x  =  y  -> 
( y  =  z  ->  A. x  y  =  z ) )
Distinct variable group:    x, y, z

Proof of Theorem ax12wK
StepHypRef Expression
1 ax-17 1628 . 2  |-  ( y  =  z  ->  A. x  y  =  z )
21a1i 12 1  |-  ( -.  x  =  y  -> 
( y  =  z  ->  A. x  y  =  z ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532
This theorem was proved from axioms:  ax-1 7  ax-mp 10  ax-17 1628
  Copyright terms: Public domain W3C validator