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

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