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  2848  gencbval  2850  clel5  2941  eqsbc2  3090  dfss  3212  dfss5  3410  rabrsndc  3737  preqr1g  3847  preqr1  3849  invdisj  4079  opthg2  4329  copsex4g  4337  opcom  4341  opeqsn  4343  opeqpr  4344  reusv3  4555  suc11g  4653  opthprc  4775  elxp3  4778  relop  4878  dmopab3  4942  rncoeq  5004  restidsing  5067  dfrel4v  5186  dmsnm  5200  iota1  5299  sniota  5315  dffn5im  5687  fvelrnb  5689  dfimafn2  5691  funimass4  5692  fnsnfv  5701  dmfco  5710  fndmdif  5748  fneqeql  5751  rexrn  5780  ralrn  5781  elrnrexdmb  5783  dffo4  5791  ftpg  5833  fconstfvm  5867  foima2  5887  rexima  5890  ralima  5891  dff13  5904  f1eqcocnv  5927  riotaeqimp  5991  eusvobj2  5999  f1ocnvfv3  6002  oprabid  6045  eloprabga  6103  ovelimab  6168  dfoprab3  6349  f1o2ndf1  6388  cnvoprab  6394  brtpos2  6412  tpossym  6437  frecsuclem  6567  nntri3or  6656  erth2  6744  brecop  6789  erovlem  6791  ecopovsym  6795  ecopovsymg  6798  xpcomco  7005  mapen  7027  nneneq  7038  supelti  7192  djuf1olem  7243  eldju  7258  omp1eomlem  7284  nninfwlporlemd  7362  exmidontriimlem3  7428  ordpipqqs  7584  addcanprg  7826  ltsrprg  7957  caucvgsrlemcl  7999  caucvgsrlemfv  8001  elreal  8038  ltresr  8049  axcaucvglemcl  8105  axcaucvglemval  8107  addsubeq4  8384  subcan2  8394  negcon1  8421  negcon2  8422  addid0  8542  divmulap2  8846  conjmulap  8899  rerecclap  8900  creur  9129  creui  9130  nndiv  9174  elznn0  9484  zltnle  9515  uzm1  9777  divfnzn  9845  zq  9850  icoshftf1o  10216  iccf1o  10229  fzen  10268  fzneuz  10326  4fvwrd4  10365  qltnle  10493  flqeqceilz  10570  modq0  10581  modqmuladdnn0  10620  addmodlteq  10650  nn0ennn  10685  uzennn  10688  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  seq3f1olemstep  10766  exp3val  10793  qsqeqor  10902  hashfacen  11090  wrd2ind  11294  cjreb  11417  caucvgrelemrec  11530  minmax  11781  xrnegiso  11813  xrnegcon1d  11815  xrminmax  11816  pwm1geoserap1  12059  dvdsval2  12341  dvdsabseq  12398  dvdsflip  12402  odd2np1  12424  oddm1even  12426  sqoddm1div8z  12437  m1exp1  12452  divalgb  12476  modremain  12480  zeqzmulgcd  12531  dfgcd2  12575  divgcdcoprm0  12663  prm2orodd  12688  hashdvds  12783  oddprmdvds  12917  oddennn  13003  evenennn  13004  gsumval2  13470  grpid  13612  grpinvcnv  13641  grplmulf1o  13647  grpsubeq0  13659  grpsubadd  13661  grplactcnv  13675  isnsg4  13789  eqg0el  13806  conjghm  13853  conjnmzb  13857  dvdsr02  14109  01eq0ring  14193  rmodislmodlem  14354  rspsn  14538  zndvds  14653  znleval  14657  psr1clfi  14692  toponsspwpwg  14736  dmtopon  14737  hmeoimaf1o  15028  txhmeo  15033  limcmpted  15377  ioocosf1o  15568  fsumdvdsmul  15705  gausslemma2dlem0i  15776  lgseisenlem2  15790  lgsquadlem2  15797  2lgslem1c  15809  2lgsoddprmlem2  15825  2lgsoddprm  15832  uspgredgiedg  16017  uspgriedgedg  16018  uspgr2wlkeq  16162  wlk0prc  16169  wlklenvclwlk  16170  bj-peano4  16486  pwle2  16535  subctctexmid  16537  pw1nct  16540  exmidsbthrlem  16562  iooref1o  16574  iswomni0  16591