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

Theorem equcomiK 28116
Description: Commutative law for equality. Uses only Tarski's FOL axiom schemes (see description for equidK 28115). 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 28115 . 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  28117  equequ2K  28118  elequ1K  28119  elequ2K  28120  ax4wfK  28131  ax4wK  28132  cbvalK  28141  cbvalvK  28142  ax7wK  28148  ax12dgen2K  28158  ax12o10lem3K  28165  equvinvK  28190  ax12olem21K  28201  equextvK  28203
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