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

Theorem equcomiK 27890
Description: Commutative law for equality. Uses only Tarski's FOL axiom schemes (see description for equidK 27889). 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 27889 . 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  27891  equequ2K  27892  elequ1K  27893  elequ2K  27894  ax4wfK  27905  ax4wK  27906  cbvalK  27915  cbvalvK  27916  ax7wK  27922  ax12dgen2K  27932  ax12o10lem3K  27939  equvinvK  27964  ax12olem21K  27975  equextvK  27977
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