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

Theorem eqcom 2141
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 1446 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
3 dfcleq 2133 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfcleq 2133 . 2 (𝐵 = 𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
52, 3, 43bitr4i 211 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1329   = wceq 1331  wcel 1480
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 1423  ax-gen 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  eqcoms  2142  eqcomi  2143  neqcomd  2144  eqcomd  2145  eqeq2  2149  eqtr2  2158  eqtr3  2159  abeq1  2249  nesym  2353  pm13.181  2390  necom  2392  gencbvex  2732  gencbval  2734  eqsbc3r  2969  dfss  3085  dfss5  3281  rabrsndc  3591  preqr1g  3693  preqr1  3695  invdisj  3923  opthg2  4161  copsex4g  4169  opcom  4172  opeqsn  4174  opeqpr  4175  reusv3  4381  suc11g  4472  opthprc  4590  elxp3  4593  relop  4689  dmopab3  4752  rncoeq  4812  dfrel4v  4990  dmsnm  5004  iota1  5102  sniota  5115  dffn5im  5467  fvelrnb  5469  dfimafn2  5471  funimass4  5472  fnsnfv  5480  dmfco  5489  fndmdif  5525  fneqeql  5528  rexrn  5557  ralrn  5558  elrnrexdmb  5560  dffo4  5568  ftpg  5604  fconstfvm  5638  foima2  5653  rexima  5656  ralima  5657  dff13  5669  f1eqcocnv  5692  eusvobj2  5760  f1ocnvfv3  5763  oprabid  5803  eloprabga  5858  ovelimab  5921  dfoprab3  6089  f1o2ndf1  6125  cnvoprab  6131  brtpos2  6148  tpossym  6173  frecsuclem  6303  nntri3or  6389  erth2  6474  brecop  6519  erovlem  6521  ecopovsym  6525  ecopovsymg  6528  xpcomco  6720  mapen  6740  nneneq  6751  supelti  6889  djuf1olem  6938  eldju  6953  omp1eomlem  6979  ordpipqqs  7196  addcanprg  7438  ltsrprg  7569  caucvgsrlemcl  7611  caucvgsrlemfv  7613  elreal  7650  ltresr  7661  axcaucvglemcl  7717  axcaucvglemval  7719  addsubeq4  7991  subcan2  8001  negcon1  8028  negcon2  8029  addid0  8149  divmulap2  8450  conjmulap  8503  rerecclap  8504  creur  8731  creui  8732  nndiv  8775  elznn0  9083  zltnle  9114  uzm1  9370  divfnzn  9427  zq  9432  icoshftf1o  9788  iccf1o  9801  fzen  9837  fzneuz  9895  4fvwrd4  9931  qltnle  10037  flqeqceilz  10105  modq0  10116  modqmuladdnn0  10155  addmodlteq  10185  nn0ennn  10220  uzennn  10223  iseqf1olemqcl  10273  iseqf1olemnab  10275  iseqf1olemab  10276  seq3f1olemstep  10288  exp3val  10309  hashfacen  10593  cjreb  10652  caucvgrelemrec  10765  minmax  11015  xrnegiso  11045  xrnegcon1d  11047  xrminmax  11048  pwm1geoserap1  11291  dvdsval2  11509  dvdsabseq  11558  dvdsflip  11562  odd2np1  11583  oddm1even  11585  sqoddm1div8z  11596  m1exp1  11611  divalgb  11635  modremain  11639  zeqzmulgcd  11672  dfgcd2  11715  divgcdcoprm0  11795  prm2orodd  11820  hashdvds  11910  oddennn  11918  evenennn  11919  toponsspwpwg  12205  dmtopon  12206  hmeoimaf1o  12499  txhmeo  12504  limcmpted  12817  ioocosf1o  12959  bj-peano4  13260  pwle2  13300  subctctexmid  13303  pw1nct  13305  exmidsbthrlem  13326
  Copyright terms: Public domain W3C validator