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

Theorem eqcom 2087
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 138 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
21albii 1402 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
3 dfcleq 2079 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfcleq 2079 . 2 (𝐵 = 𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
52, 3, 43bitr4i 210 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1285   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqcoms  2088  eqcomi  2089  eqcomd  2090  eqeq2  2094  eqtr2  2103  eqtr3  2104  abeq1  2194  nesym  2296  pm13.181  2333  necom  2335  gencbvex  2659  gencbval  2661  eqsbc3r  2888  dfss  3002  dfss5  3194  rabrsndc  3492  preqr1g  3592  preqr1  3594  invdisj  3814  opthg2  4038  copsex4g  4046  opcom  4049  opeqsn  4051  opeqpr  4052  reusv3  4254  suc11g  4344  opthprc  4455  elxp3  4458  relop  4552  dmopab3  4615  rncoeq  4672  dfrel4v  4844  dmsnm  4858  iota1  4956  sniota  4969  dffn5im  5306  fvelrnb  5308  dfimafn2  5310  funimass4  5311  fnsnfv  5319  dmfco  5328  fndmdif  5360  fneqeql  5363  rexrn  5392  ralrn  5393  elrnrexdmb  5395  dffo4  5403  ftpg  5437  fconstfvm  5469  foima2  5484  rexima  5488  ralima  5489  dff13  5501  f1eqcocnv  5524  eusvobj2  5592  f1ocnvfv3  5595  oprabid  5631  eloprabga  5685  ovelimab  5745  dfoprab3  5911  f1o2ndf1  5943  cnvoprab  5949  brtpos2  5963  tpossym  5988  frecsuclem  6118  nntri3or  6201  erth2  6282  brecop  6327  erovlem  6329  ecopovsym  6333  ecopovsymg  6336  xpcomco  6487  mapen  6507  nneneq  6518  supelti  6633  djuf1olem  6681  eldju  6695  ordpipqqs  6869  addcanprg  7111  ltsrprg  7229  caucvgsrlemcl  7270  caucvgsrlemfv  7272  elreal  7302  ltresr  7312  axcaucvglemcl  7366  axcaucvglemval  7368  addsubeq4  7633  subcan2  7643  negcon1  7670  negcon2  7671  addid0  7787  divmulap2  8074  conjmulap  8127  rerecclap  8128  creur  8346  creui  8347  nndiv  8389  elznn0  8690  zltnle  8721  uzm1  8973  divfnzn  9030  zq  9035  icoshftf1o  9332  iccf1o  9345  fzen  9381  fzneuz  9437  4fvwrd4  9471  qltnle  9577  flqeqceilz  9645  modq0  9656  modqmuladdnn0  9695  addmodlteq  9725  nn0ennn  9760  iseqf1olemqcl  9811  iseqf1olemnab  9813  iseqf1olemab  9814  iseqf1olemstep  9826  hashfacen  10129  cjreb  10187  caucvgrelemrec  10299  minmax  10546  dvdsval2  10665  dvdsabseq  10714  dvdsflip  10718  odd2np1  10739  oddm1even  10741  sqoddm1div8z  10752  m1exp1  10767  divalgb  10791  modremain  10795  zeqzmulgcd  10828  dfgcd2  10869  divgcdcoprm0  10949  prm2orodd  10974  hashdvds  11063  oddennn  11071  evenennn  11072  bj-peano4  11279  exmidsbthrlem  11341
  Copyright terms: Public domain W3C validator