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  4294  opeqsn  4296  opeqpr  4297  reusv3  4506  suc11g  4604  opthprc  4725  elxp3  4728  relop  4827  dmopab3  4890  rncoeq  4951  restidsing  5014  dfrel4v  5133  dmsnm  5147  iota1  5245  sniota  5261  dffn5im  5623  fvelrnb  5625  dfimafn2  5627  funimass4  5628  fnsnfv  5637  dmfco  5646  fndmdif  5684  fneqeql  5687  rexrn  5716  ralrn  5717  elrnrexdmb  5719  dffo4  5727  ftpg  5767  fconstfvm  5801  foima2  5819  rexima  5822  ralima  5823  dff13  5836  f1eqcocnv  5859  eusvobj2  5929  f1ocnvfv3  5932  oprabid  5975  eloprabga  6031  ovelimab  6096  dfoprab3  6276  f1o2ndf1  6313  cnvoprab  6319  brtpos2  6336  tpossym  6361  frecsuclem  6491  nntri3or  6578  erth2  6666  brecop  6711  erovlem  6713  ecopovsym  6717  ecopovsymg  6720  xpcomco  6920  mapen  6942  nneneq  6953  supelti  7103  djuf1olem  7154  eldju  7169  omp1eomlem  7195  nninfwlporlemd  7273  exmidontriimlem3  7334  ordpipqqs  7486  addcanprg  7728  ltsrprg  7859  caucvgsrlemcl  7901  caucvgsrlemfv  7903  elreal  7940  ltresr  7951  axcaucvglemcl  8007  axcaucvglemval  8009  addsubeq4  8286  subcan2  8296  negcon1  8323  negcon2  8324  addid0  8444  divmulap2  8748  conjmulap  8801  rerecclap  8802  creur  9031  creui  9032  nndiv  9076  elznn0  9386  zltnle  9417  uzm1  9678  divfnzn  9741  zq  9746  icoshftf1o  10112  iccf1o  10125  fzen  10164  fzneuz  10222  4fvwrd4  10261  qltnle  10384  flqeqceilz  10461  modq0  10472  modqmuladdnn0  10511  addmodlteq  10541  nn0ennn  10576  uzennn  10579  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  seq3f1olemstep  10657  exp3val  10684  qsqeqor  10793  hashfacen  10979  cjreb  11119  caucvgrelemrec  11232  minmax  11483  xrnegiso  11515  xrnegcon1d  11517  xrminmax  11518  pwm1geoserap1  11761  dvdsval2  12043  dvdsabseq  12100  dvdsflip  12104  odd2np1  12126  oddm1even  12128  sqoddm1div8z  12139  m1exp1  12154  divalgb  12178  modremain  12182  zeqzmulgcd  12233  dfgcd2  12277  divgcdcoprm0  12365  prm2orodd  12390  hashdvds  12485  oddprmdvds  12619  oddennn  12705  evenennn  12706  gsumval2  13171  grpid  13313  grpinvcnv  13342  grplmulf1o  13348  grpsubeq0  13360  grpsubadd  13362  grplactcnv  13376  isnsg4  13490  eqg0el  13507  conjghm  13554  conjnmzb  13558  dvdsr02  13809  01eq0ring  13893  rmodislmodlem  14054  rspsn  14238  zndvds  14353  znleval  14357  psr1clfi  14392  toponsspwpwg  14436  dmtopon  14437  hmeoimaf1o  14728  txhmeo  14733  limcmpted  15077  ioocosf1o  15268  fsumdvdsmul  15405  gausslemma2dlem0i  15476  lgseisenlem2  15490  lgsquadlem2  15497  2lgslem1c  15509  2lgsoddprmlem2  15525  2lgsoddprm  15532  bj-peano4  15824  pwle2  15868  subctctexmid  15870  pw1nct  15873  exmidsbthrlem  15894  iooref1o  15906  iswomni0  15923