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

Theorem equcomiK 28137
Description: Commutative law for equality. Uses only Tarski's FOL axiom schemes (see description for equidK 28136). 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 28136 . 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  28138  equequ2K  28139  elequ1K  28140  elequ2K  28141  ax4wfK  28152  ax4wK  28153  cbvalK  28162  cbvalvK  28163  ax7wK  28169  ax12dgen2K  28179  ax12o10lem3K  28186  equvinvK  28211  ax12olem21K  28222  equextvK  28224
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