ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqcom Unicode version

Theorem eqcom 2042
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqcom  |-  ( A  =  B  <->  B  =  A )

Proof of Theorem eqcom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 bicom 128 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1359 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2034 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2034 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 201 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 98   A.wal 1241    = wceq 1243    e. wcel 1393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqcoms  2043  eqcomi  2044  eqcomd  2045  eqeq2  2049  eqtr2  2058  eqtr3  2059  abeq1  2147  nesym  2247  pm13.181  2284  necom  2286  gencbvex  2597  gencbval  2599  eqsbc3r  2816  dfss  2929  dfss5  3139  disj4im  3273  ssnelpss  3286  rabrsndc  3435  preqr1g  3534  preqr1  3536  invdisj  3756  opthg2  3973  copsex4g  3981  opcom  3984  opeqsn  3986  opeqpr  3987  reusv3  4179  suc11g  4266  dtruex  4268  opthprc  4369  elxp3  4372  relop  4464  dmopab3  4526  rncoeq  4583  dfrel4v  4750  dmsnm  4764  iota1  4859  sniota  4872  dffn5im  5197  fvelrnb  5199  dfimafn2  5201  funimass4  5202  fnsnfv  5210  dmfco  5219  fndmdif  5250  fneqeql  5253  rexrn  5282  ralrn  5283  elrnrexdmb  5285  dffo4  5293  ftpg  5325  fconstfvm  5357  rexima  5372  ralima  5373  dff13  5385  f1eqcocnv  5409  eusvobj2  5476  f1ocnvfv3  5479  oprabid  5515  eloprabga  5569  ovelimab  5629  dfoprab3  5795  f1o2ndf1  5827  brtpos2  5844  tpossym  5869  frecsuclem3  5968  nntri3or  6050  erth2  6129  brecop  6174  erovlem  6176  ecopovsym  6180  ecopovsymg  6183  xpcomco  6278  nneneq  6298  ordpipqqs  6444  addcanprg  6686  ltsrprg  6804  caucvgsrlemcl  6845  caucvgsrlemfv  6847  elreal  6877  ltresr  6887  axcaucvglemcl  6941  axcaucvglemval  6943  addsubeq4  7197  subcan2  7206  negcon1  7233  negcon2  7234  divmulap2  7622  conjmulap  7672  rerecclap  7673  creur  7878  creui  7879  nndiv  7921  elznn0  8223  zltnle  8254  uzm1  8466  divfnzn  8519  zq  8524  icoshftf1o  8817  iccf1o  8830  fzen  8865  fzneuz  8921  4fvwrd4  8955  nn0ennn  9078  cjreb  9335  caucvgrelemrec  9447  bj-peano4  9944
  Copyright terms: Public domain W3C validator