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

Theorem ax12wK 28276
Description: Weak version (principal instance) of ax-12 1633 not involving bundling. Uses only Tarski's FOL axiom schemes (see description for equidK 28235). The proof is trivial but is included to complete the set ax6wK 28265, ax7wK 28268, and ax11wK 28273. See the description in the comment of equidK 28235. (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