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

Theorem ax12wK 27827
Description: Weak version (principal instance) of ax-12 1633 not involving bundling. Uses only Tarski's predicate calculus axiom schemes. The proof is trivial but is included to complete the set ax6wK 27816, ax7wK 27819, and ax11wK 27824. See the description in the comment of equidK 27792. (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