Theorem eqcom 2177

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.

Step	Hyp	Ref	Expression
1		bicom 140	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
2	1	albii 1468	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2169	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2169	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 105  ∀wal 1351   = wceq 1353   ∈ wcel 2146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168

This theorem is referenced by:  eqcoms  2178  eqcomi  2179  neqcomd  2180  eqcomd  2181  eqeq2  2185  eqtr2  2194  eqtr3  2195  abeq1  2285  nesym  2390  pm13.181  2427  necom  2429  gencbvex  2781  gencbval  2783  clel5  2872  eqsbc2  3021  dfss  3141  dfss5  3338  rabrsndc  3657  preqr1g  3762  preqr1  3764  invdisj  3992  opthg2  4233  copsex4g  4241  opcom  4244  opeqsn  4246  opeqpr  4247  reusv3  4454  suc11g  4550  opthprc  4671  elxp3  4674  relop  4770  dmopab3  4833  rncoeq  4893  restidsing  4956  dfrel4v  5072  dmsnm  5086  iota1  5184  sniota  5199  dffn5im  5553  fvelrnb  5555  dfimafn2  5557  funimass4  5558  fnsnfv  5567  dmfco  5576  fndmdif  5613  fneqeql  5616  rexrn  5645  ralrn  5646  elrnrexdmb  5648  dffo4  5656  ftpg  5692  fconstfvm  5726  foima2  5743  rexima  5746  ralima  5747  dff13  5759  f1eqcocnv  5782  eusvobj2  5851  f1ocnvfv3  5854  oprabid  5897  eloprabga  5952  ovelimab  6015  dfoprab3  6182  f1o2ndf1  6219  cnvoprab  6225  brtpos2  6242  tpossym  6267  frecsuclem  6397  nntri3or  6484  erth2  6570  brecop  6615  erovlem  6617  ecopovsym  6621  ecopovsymg  6624  xpcomco  6816  mapen  6836  nneneq  6847  supelti  6991  djuf1olem  7042  eldju  7057  omp1eomlem  7083  nninfwlporlemd  7160  exmidontriimlem3  7212  ordpipqqs  7348  addcanprg  7590  ltsrprg  7721  caucvgsrlemcl  7763  caucvgsrlemfv  7765  elreal  7802  ltresr  7813  axcaucvglemcl  7869  axcaucvglemval  7871  addsubeq4  8146  subcan2  8156  negcon1  8183  negcon2  8184  addid0  8304  divmulap2  8606  conjmulap  8659  rerecclap  8660  creur  8889  creui  8890  nndiv  8933  elznn0  9241  zltnle  9272  uzm1  9531  divfnzn  9594  zq  9599  icoshftf1o  9962  iccf1o  9975  fzen  10013  fzneuz  10071  4fvwrd4  10110  qltnle  10216  flqeqceilz  10288  modq0  10299  modqmuladdnn0  10338  addmodlteq  10368  nn0ennn  10403  uzennn  10406  iseqf1olemqcl  10456  iseqf1olemnab  10458  iseqf1olemab  10459  seq3f1olemstep  10471  exp3val  10492  qsqeqor  10600  hashfacen  10784  cjreb  10843  caucvgrelemrec  10956  minmax  11206  xrnegiso  11238  xrnegcon1d  11240  xrminmax  11241  pwm1geoserap1  11484  dvdsval2  11765  dvdsabseq  11820  dvdsflip  11824  odd2np1  11845  oddm1even  11847  sqoddm1div8z  11858  m1exp1  11873  divalgb  11897  modremain  11901  zeqzmulgcd  11938  dfgcd2  11982  divgcdcoprm0  12068  prm2orodd  12093  hashdvds  12188  oddprmdvds  12319  oddennn  12360  evenennn  12361  grpid  12774  grpinvcnv  12799  grplmulf1o  12805  grpsubeq0  12817  grpsubadd  12819  grplactcnv  12833  toponsspwpwg  13091  dmtopon  13092  hmeoimaf1o  13385  txhmeo  13390  limcmpted  13703  ioocosf1o  13846  bj-peano4  14267  pwle2  14308  subctctexmid  14311  pw1nct  14313  exmidsbthrlem  14331  iooref1o  14343  iswomni0  14360