Theorem eqcom 2198

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 1484	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2190	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2190	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqcoms  2199  eqcomi  2200  neqcomd  2201  eqcomd  2202  eqeq2  2206  eqtr2  2215  eqtr3  2216  abeq1  2306  nesym  2412  pm13.181  2449  necom  2451  gencbvex  2810  gencbval  2812  clel5  2901  eqsbc2  3050  dfss  3171  dfss5  3369  rabrsndc  3691  preqr1g  3797  preqr1  3799  invdisj  4028  opthg2  4273  copsex4g  4281  opcom  4284  opeqsn  4286  opeqpr  4287  reusv3  4496  suc11g  4594  opthprc  4715  elxp3  4718  relop  4817  dmopab3  4880  rncoeq  4940  restidsing  5003  dfrel4v  5122  dmsnm  5136  iota1  5234  sniota  5250  dffn5im  5609  fvelrnb  5611  dfimafn2  5613  funimass4  5614  fnsnfv  5623  dmfco  5632  fndmdif  5670  fneqeql  5673  rexrn  5702  ralrn  5703  elrnrexdmb  5705  dffo4  5713  ftpg  5749  fconstfvm  5783  foima2  5801  rexima  5804  ralima  5805  dff13  5818  f1eqcocnv  5841  eusvobj2  5911  f1ocnvfv3  5914  oprabid  5957  eloprabga  6013  ovelimab  6078  dfoprab3  6258  f1o2ndf1  6295  cnvoprab  6301  brtpos2  6318  tpossym  6343  frecsuclem  6473  nntri3or  6560  erth2  6648  brecop  6693  erovlem  6695  ecopovsym  6699  ecopovsymg  6702  xpcomco  6894  mapen  6916  nneneq  6927  supelti  7077  djuf1olem  7128  eldju  7143  omp1eomlem  7169  nninfwlporlemd  7247  exmidontriimlem3  7308  ordpipqqs  7460  addcanprg  7702  ltsrprg  7833  caucvgsrlemcl  7875  caucvgsrlemfv  7877  elreal  7914  ltresr  7925  axcaucvglemcl  7981  axcaucvglemval  7983  addsubeq4  8260  subcan2  8270  negcon1  8297  negcon2  8298  addid0  8418  divmulap2  8722  conjmulap  8775  rerecclap  8776  creur  9005  creui  9006  nndiv  9050  elznn0  9360  zltnle  9391  uzm1  9651  divfnzn  9714  zq  9719  icoshftf1o  10085  iccf1o  10098  fzen  10137  fzneuz  10195  4fvwrd4  10234  qltnle  10352  flqeqceilz  10429  modq0  10440  modqmuladdnn0  10479  addmodlteq  10509  nn0ennn  10544  uzennn  10547  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  seq3f1olemstep  10625  exp3val  10652  qsqeqor  10761  hashfacen  10947  cjreb  11050  caucvgrelemrec  11163  minmax  11414  xrnegiso  11446  xrnegcon1d  11448  xrminmax  11449  pwm1geoserap1  11692  dvdsval2  11974  dvdsabseq  12031  dvdsflip  12035  odd2np1  12057  oddm1even  12059  sqoddm1div8z  12070  m1exp1  12085  divalgb  12109  modremain  12113  zeqzmulgcd  12164  dfgcd2  12208  divgcdcoprm0  12296  prm2orodd  12321  hashdvds  12416  oddprmdvds  12550  oddennn  12636  evenennn  12637  gsumval2  13101  grpid  13243  grpinvcnv  13272  grplmulf1o  13278  grpsubeq0  13290  grpsubadd  13292  grplactcnv  13306  isnsg4  13420  eqg0el  13437  conjghm  13484  conjnmzb  13488  dvdsr02  13739  01eq0ring  13823  rmodislmodlem  13984  rspsn  14168  zndvds  14283  znleval  14287  psr1clfi  14322  toponsspwpwg  14366  dmtopon  14367  hmeoimaf1o  14658  txhmeo  14663  limcmpted  15007  ioocosf1o  15198  fsumdvdsmul  15335  gausslemma2dlem0i  15406  lgseisenlem2  15420  lgsquadlem2  15427  2lgslem1c  15439  2lgsoddprmlem2  15455  2lgsoddprm  15462  bj-peano4  15709  pwle2  15753  subctctexmid  15755  pw1nct  15758  exmidsbthrlem  15779  iooref1o  15791  iswomni0  15808