Theorem eqcom 2206

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

Syntax hints:   ↔ wb 105  ∀wal 1370   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ext 2186

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

This theorem is referenced by:  eqcoms  2207  eqcomi  2208  neqcomd  2209  eqcomd  2210  eqeq2  2214  eqtr2  2223  eqtr3  2224  abeq1  2314  nesym  2420  pm13.181  2457  necom  2459  gencbvex  2818  gencbval  2820  clel5  2909  eqsbc2  3058  dfss  3179  dfss5  3377  rabrsndc  3700  preqr1g  3806  preqr1  3808  invdisj  4037  opthg2  4282  copsex4g  4290  opcom  4293  opeqsn  4295  opeqpr  4296  reusv3  4505  suc11g  4603  opthprc  4724  elxp3  4727  relop  4826  dmopab3  4889  rncoeq  4949  restidsing  5012  dfrel4v  5131  dmsnm  5145  iota1  5243  sniota  5259  dffn5im  5618  fvelrnb  5620  dfimafn2  5622  funimass4  5623  fnsnfv  5632  dmfco  5641  fndmdif  5679  fneqeql  5682  rexrn  5711  ralrn  5712  elrnrexdmb  5714  dffo4  5722  ftpg  5758  fconstfvm  5792  foima2  5810  rexima  5813  ralima  5814  dff13  5827  f1eqcocnv  5850  eusvobj2  5920  f1ocnvfv3  5923  oprabid  5966  eloprabga  6022  ovelimab  6087  dfoprab3  6267  f1o2ndf1  6304  cnvoprab  6310  brtpos2  6327  tpossym  6352  frecsuclem  6482  nntri3or  6569  erth2  6657  brecop  6702  erovlem  6704  ecopovsym  6708  ecopovsymg  6711  xpcomco  6903  mapen  6925  nneneq  6936  supelti  7086  djuf1olem  7137  eldju  7152  omp1eomlem  7178  nninfwlporlemd  7256  exmidontriimlem3  7317  ordpipqqs  7469  addcanprg  7711  ltsrprg  7842  caucvgsrlemcl  7884  caucvgsrlemfv  7886  elreal  7923  ltresr  7934  axcaucvglemcl  7990  axcaucvglemval  7992  addsubeq4  8269  subcan2  8279  negcon1  8306  negcon2  8307  addid0  8427  divmulap2  8731  conjmulap  8784  rerecclap  8785  creur  9014  creui  9015  nndiv  9059  elznn0  9369  zltnle  9400  uzm1  9661  divfnzn  9724  zq  9729  icoshftf1o  10095  iccf1o  10108  fzen  10147  fzneuz  10205  4fvwrd4  10244  qltnle  10367  flqeqceilz  10444  modq0  10455  modqmuladdnn0  10494  addmodlteq  10524  nn0ennn  10559  uzennn  10562  iseqf1olemqcl  10625  iseqf1olemnab  10627  iseqf1olemab  10628  seq3f1olemstep  10640  exp3val  10667  qsqeqor  10776  hashfacen  10962  cjreb  11096  caucvgrelemrec  11209  minmax  11460  xrnegiso  11492  xrnegcon1d  11494  xrminmax  11495  pwm1geoserap1  11738  dvdsval2  12020  dvdsabseq  12077  dvdsflip  12081  odd2np1  12103  oddm1even  12105  sqoddm1div8z  12116  m1exp1  12131  divalgb  12155  modremain  12159  zeqzmulgcd  12210  dfgcd2  12254  divgcdcoprm0  12342  prm2orodd  12367  hashdvds  12462  oddprmdvds  12596  oddennn  12682  evenennn  12683  gsumval2  13147  grpid  13289  grpinvcnv  13318  grplmulf1o  13324  grpsubeq0  13336  grpsubadd  13338  grplactcnv  13352  isnsg4  13466  eqg0el  13483  conjghm  13530  conjnmzb  13534  dvdsr02  13785  01eq0ring  13869  rmodislmodlem  14030  rspsn  14214  zndvds  14329  znleval  14333  psr1clfi  14368  toponsspwpwg  14412  dmtopon  14413  hmeoimaf1o  14704  txhmeo  14709  limcmpted  15053  ioocosf1o  15244  fsumdvdsmul  15381  gausslemma2dlem0i  15452  lgseisenlem2  15466  lgsquadlem2  15473  2lgslem1c  15485  2lgsoddprmlem2  15501  2lgsoddprm  15508  bj-peano4  15755  pwle2  15799  subctctexmid  15801  pw1nct  15804  exmidsbthrlem  15825  iooref1o  15837  iswomni0  15854