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

Theorem equcomiK 27793
Description: Commutative law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 3 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.)
Assertion
Ref Expression
equcomiK  |-  ( x  =  y  ->  y  =  x )

Proof of Theorem equcomiK
StepHypRef Expression
1 equidK 27792 . 2  |-  x  =  x
2 ax-8 1623 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
31, 2mpi 18 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  equequ1K  27794  equequ2K  27795  elequ1K  27796  elequ2K  27797  ax4wfK  27806  ax4wK  27807  cbvalK  27812  cbvalvK  27813  ax7wK  27819  ax12dgen2K  27829  ax12o10lem3K  27836  equvinvK  27861  ax12olem21K  27872  equextvK  27874
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9v 1632
  Copyright terms: Public domain W3C validator