Theorem eqcom 2231

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

Syntax hints:   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqcoms  2232  eqcomi  2233  neqcomd  2234  eqcomd  2235  eqeq2  2239  eqtr2  2248  eqtr3  2249  abeq1  2339  nesym  2445  pm13.181  2482  necom  2484  gencbvex  2847  gencbval  2849  clel5  2940  eqsbc2  3089  dfss  3211  dfss5  3409  rabrsndc  3734  preqr1g  3844  preqr1  3846  invdisj  4076  opthg2  4325  copsex4g  4333  opcom  4337  opeqsn  4339  opeqpr  4340  reusv3  4551  suc11g  4649  opthprc  4770  elxp3  4773  relop  4872  dmopab3  4936  rncoeq  4998  restidsing  5061  dfrel4v  5180  dmsnm  5194  iota1  5293  sniota  5309  dffn5im  5681  fvelrnb  5683  dfimafn2  5685  funimass4  5686  fnsnfv  5695  dmfco  5704  fndmdif  5742  fneqeql  5745  rexrn  5774  ralrn  5775  elrnrexdmb  5777  dffo4  5785  ftpg  5827  fconstfvm  5861  foima2  5881  rexima  5884  ralima  5885  dff13  5898  f1eqcocnv  5921  riotaeqimp  5985  eusvobj2  5993  f1ocnvfv3  5996  oprabid  6039  eloprabga  6097  ovelimab  6162  dfoprab3  6343  f1o2ndf1  6380  cnvoprab  6386  brtpos2  6403  tpossym  6428  frecsuclem  6558  nntri3or  6647  erth2  6735  brecop  6780  erovlem  6782  ecopovsym  6786  ecopovsymg  6789  xpcomco  6993  mapen  7015  nneneq  7026  supelti  7180  djuf1olem  7231  eldju  7246  omp1eomlem  7272  nninfwlporlemd  7350  exmidontriimlem3  7416  ordpipqqs  7572  addcanprg  7814  ltsrprg  7945  caucvgsrlemcl  7987  caucvgsrlemfv  7989  elreal  8026  ltresr  8037  axcaucvglemcl  8093  axcaucvglemval  8095  addsubeq4  8372  subcan2  8382  negcon1  8409  negcon2  8410  addid0  8530  divmulap2  8834  conjmulap  8887  rerecclap  8888  creur  9117  creui  9118  nndiv  9162  elznn0  9472  zltnle  9503  uzm1  9765  divfnzn  9828  zq  9833  icoshftf1o  10199  iccf1o  10212  fzen  10251  fzneuz  10309  4fvwrd4  10348  qltnle  10475  flqeqceilz  10552  modq0  10563  modqmuladdnn0  10602  addmodlteq  10632  nn0ennn  10667  uzennn  10670  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  seq3f1olemstep  10748  exp3val  10775  qsqeqor  10884  hashfacen  11071  wrd2ind  11270  cjreb  11392  caucvgrelemrec  11505  minmax  11756  xrnegiso  11788  xrnegcon1d  11790  xrminmax  11791  pwm1geoserap1  12034  dvdsval2  12316  dvdsabseq  12373  dvdsflip  12377  odd2np1  12399  oddm1even  12401  sqoddm1div8z  12412  m1exp1  12427  divalgb  12451  modremain  12455  zeqzmulgcd  12506  dfgcd2  12550  divgcdcoprm0  12638  prm2orodd  12663  hashdvds  12758  oddprmdvds  12892  oddennn  12978  evenennn  12979  gsumval2  13445  grpid  13587  grpinvcnv  13616  grplmulf1o  13622  grpsubeq0  13634  grpsubadd  13636  grplactcnv  13650  isnsg4  13764  eqg0el  13781  conjghm  13828  conjnmzb  13832  dvdsr02  14084  01eq0ring  14168  rmodislmodlem  14329  rspsn  14513  zndvds  14628  znleval  14632  psr1clfi  14667  toponsspwpwg  14711  dmtopon  14712  hmeoimaf1o  15003  txhmeo  15008  limcmpted  15352  ioocosf1o  15543  fsumdvdsmul  15680  gausslemma2dlem0i  15751  lgseisenlem2  15765  lgsquadlem2  15772  2lgslem1c  15784  2lgsoddprmlem2  15800  2lgsoddprm  15807  uspgredgiedg  15991  uspgriedgedg  15992  uspgr2wlkeq  16106  wlk0prc  16113  wlklenvclwlk  16114  bj-peano4  16373  pwle2  16423  subctctexmid  16425  pw1nct  16428  exmidsbthrlem  16450  iooref1o  16462  iswomni0  16479