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

Theorem eqcom 2119
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqcom (𝐴 = 𝐵𝐵 = 𝐴)

Proof of Theorem eqcom
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 bicom 139 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
21albii 1431 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
3 dfcleq 2111 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfcleq 2111 . 2 (𝐵 = 𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
52, 3, 43bitr4i 211 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1314   = wceq 1316  wcel 1465
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 1408  ax-gen 1410  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqcoms  2120  eqcomi  2121  neqcomd  2122  eqcomd  2123  eqeq2  2127  eqtr2  2136  eqtr3  2137  abeq1  2227  nesym  2330  pm13.181  2367  necom  2369  gencbvex  2706  gencbval  2708  eqsbc3r  2941  dfss  3055  dfss5  3251  rabrsndc  3561  preqr1g  3663  preqr1  3665  invdisj  3893  opthg2  4131  copsex4g  4139  opcom  4142  opeqsn  4144  opeqpr  4145  reusv3  4351  suc11g  4442  opthprc  4560  elxp3  4563  relop  4659  dmopab3  4722  rncoeq  4782  dfrel4v  4960  dmsnm  4974  iota1  5072  sniota  5085  dffn5im  5435  fvelrnb  5437  dfimafn2  5439  funimass4  5440  fnsnfv  5448  dmfco  5457  fndmdif  5493  fneqeql  5496  rexrn  5525  ralrn  5526  elrnrexdmb  5528  dffo4  5536  ftpg  5572  fconstfvm  5606  foima2  5621  rexima  5624  ralima  5625  dff13  5637  f1eqcocnv  5660  eusvobj2  5728  f1ocnvfv3  5731  oprabid  5771  eloprabga  5826  ovelimab  5889  dfoprab3  6057  f1o2ndf1  6093  cnvoprab  6099  brtpos2  6116  tpossym  6141  frecsuclem  6271  nntri3or  6357  erth2  6442  brecop  6487  erovlem  6489  ecopovsym  6493  ecopovsymg  6496  xpcomco  6688  mapen  6708  nneneq  6719  supelti  6857  djuf1olem  6906  eldju  6921  omp1eomlem  6947  ordpipqqs  7150  addcanprg  7392  ltsrprg  7523  caucvgsrlemcl  7565  caucvgsrlemfv  7567  elreal  7604  ltresr  7615  axcaucvglemcl  7671  axcaucvglemval  7673  addsubeq4  7945  subcan2  7955  negcon1  7982  negcon2  7983  addid0  8103  divmulap2  8403  conjmulap  8456  rerecclap  8457  creur  8681  creui  8682  nndiv  8725  elznn0  9027  zltnle  9058  uzm1  9312  divfnzn  9369  zq  9374  icoshftf1o  9729  iccf1o  9742  fzen  9778  fzneuz  9836  4fvwrd4  9872  qltnle  9978  flqeqceilz  10046  modq0  10057  modqmuladdnn0  10096  addmodlteq  10126  nn0ennn  10161  uzennn  10164  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  seq3f1olemstep  10229  exp3val  10250  hashfacen  10534  cjreb  10593  caucvgrelemrec  10706  minmax  10956  xrnegiso  10986  xrnegcon1d  10988  xrminmax  10989  pwm1geoserap1  11232  dvdsval2  11408  dvdsabseq  11457  dvdsflip  11461  odd2np1  11482  oddm1even  11484  sqoddm1div8z  11495  m1exp1  11510  divalgb  11534  modremain  11538  zeqzmulgcd  11571  dfgcd2  11614  divgcdcoprm0  11694  prm2orodd  11719  hashdvds  11808  oddennn  11816  evenennn  11817  toponsspwpwg  12100  dmtopon  12101  hmeoimaf1o  12394  txhmeo  12399  limcmpted  12712  bj-peano4  13049  pwle2  13089  subctctexmid  13092  exmidsbthrlem  13113
  Copyright terms: Public domain W3C validator