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

Theorem eqcom 2117
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 139 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1429 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2109 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2109 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 211 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1312    = wceq 1314    e. wcel 1463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  eqcoms  2118  eqcomi  2119  neqcomd  2120  eqcomd  2121  eqeq2  2125  eqtr2  2134  eqtr3  2135  abeq1  2225  nesym  2328  pm13.181  2365  necom  2367  gencbvex  2704  gencbval  2706  eqsbc3r  2939  dfss  3053  dfss5  3249  rabrsndc  3559  preqr1g  3661  preqr1  3663  invdisj  3891  opthg2  4129  copsex4g  4137  opcom  4140  opeqsn  4142  opeqpr  4143  reusv3  4349  suc11g  4440  opthprc  4558  elxp3  4561  relop  4657  dmopab3  4720  rncoeq  4780  dfrel4v  4958  dmsnm  4972  iota1  5070  sniota  5083  dffn5im  5433  fvelrnb  5435  dfimafn2  5437  funimass4  5438  fnsnfv  5446  dmfco  5455  fndmdif  5491  fneqeql  5494  rexrn  5523  ralrn  5524  elrnrexdmb  5526  dffo4  5534  ftpg  5570  fconstfvm  5604  foima2  5619  rexima  5622  ralima  5623  dff13  5635  f1eqcocnv  5658  eusvobj2  5726  f1ocnvfv3  5729  oprabid  5769  eloprabga  5824  ovelimab  5887  dfoprab3  6055  f1o2ndf1  6091  cnvoprab  6097  brtpos2  6114  tpossym  6139  frecsuclem  6269  nntri3or  6355  erth2  6440  brecop  6485  erovlem  6487  ecopovsym  6491  ecopovsymg  6494  xpcomco  6686  mapen  6706  nneneq  6717  supelti  6855  djuf1olem  6904  eldju  6919  omp1eomlem  6945  ordpipqqs  7146  addcanprg  7388  ltsrprg  7519  caucvgsrlemcl  7561  caucvgsrlemfv  7563  elreal  7600  ltresr  7611  axcaucvglemcl  7667  axcaucvglemval  7669  addsubeq4  7941  subcan2  7951  negcon1  7978  negcon2  7979  addid0  8099  divmulap2  8396  conjmulap  8449  rerecclap  8450  creur  8674  creui  8675  nndiv  8718  elznn0  9020  zltnle  9051  uzm1  9305  divfnzn  9362  zq  9367  icoshftf1o  9714  iccf1o  9727  fzen  9763  fzneuz  9821  4fvwrd4  9857  qltnle  9963  flqeqceilz  10031  modq0  10042  modqmuladdnn0  10081  addmodlteq  10111  nn0ennn  10146  uzennn  10149  iseqf1olemqcl  10199  iseqf1olemnab  10201  iseqf1olemab  10202  seq3f1olemstep  10214  exp3val  10235  hashfacen  10519  cjreb  10578  caucvgrelemrec  10691  minmax  10941  xrnegiso  10971  xrnegcon1d  10973  xrminmax  10974  pwm1geoserap1  11217  dvdsval2  11392  dvdsabseq  11441  dvdsflip  11445  odd2np1  11466  oddm1even  11468  sqoddm1div8z  11479  m1exp1  11494  divalgb  11518  modremain  11522  zeqzmulgcd  11555  dfgcd2  11598  divgcdcoprm0  11678  prm2orodd  11703  hashdvds  11792  oddennn  11800  evenennn  11801  toponsspwpwg  12084  dmtopon  12085  hmeoimaf1o  12378  txhmeo  12383  limcmpted  12696  bj-peano4  12976  pwle2  13016  subctctexmid  13019  exmidsbthrlem  13040
  Copyright terms: Public domain W3C validator