Theorem eqcom 2240

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

This proof depends on syntax axioms:   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqcoms  2241  eqcomi  2242  neqcomd  2243  eqcomd  2244  eqeq2  2248  eqtr2  2257  eqtr3  2258  abeq1  2348  eqabcbw  2376  eqabcb  2377  nesym  2465  pm13.181  2502  necom  2504  gencbvex  2869  gencbval  2871  clel5  2963  eqsbc2  3112  dfss  3234  dfss5  3436  rabrsndc  3779  preqr1g  3891  preqr1  3893  invdisj  4123  opthg2  4381  copsex4g  4389  opcom  4393  opeqsn  4395  opeqpr  4396  reusv3  4608  suc11g  4706  opthprc  4828  elxp3  4831  relop  4932  dmopab3  4996  rncoeq  5058  restidsing  5122  dfrel4v  5242  dmsnm  5256  iota1  5355  sniota  5371  dffn5im  5751  fvelrnb  5753  dfimafn2  5755  funimass4  5756  fnsnfv  5765  dmfco  5776  fndmdif  5817  fneqeql  5820  rexrn  5848  ralrn  5849  elrnrexdmb  5851  dffo4  5859  ftpg  5902  fconstfvm  5936  dfimafnf  5958  foima2  5960  rexima  5963  ralima  5964  dff13  5977  f1eqcocnv  6000  riotaeqimp  6066  eusvobj2  6074  f1ocnvfv3  6077  oprabid  6120  eloprabga  6178  ovelimab  6243  dfoprab3  6429  f1o2ndf1  6468  cnvoprab  6474  brtpos2  6527  tpossym  6552  frecsuclem  6682  nntri3or  6771  erth2  6859  brecop  6904  erovlem  6906  ecopovsym  6910  ecopovsymg  6913  xpcomco  7130  mapen  7152  nneneq  7164  supelti  7348  djuf1olem  7399  eldju  7414  omp1eomlem  7440  nninfwlporlemd  7518  exmidontriimlem3  7585  ordpipqqs  7747  addcanprg  7989  ltsrprg  8120  caucvgsrlemcl  8162  caucvgsrlemfv  8164  elreal  8201  ltresr  8212  axcaucvglemcl  8268  axcaucvglemval  8270  addsubeq4  8548  subcan2  8558  negcon1  8585  negcon2  8586  addid0  8706  addeq0  8710  divmulap2  9014  conjmulap  9067  rerecclap  9068  creur  9297  creui  9298  nndiv  9354  elznn0  9668  zltnle  9699  uzm1  9968  divfnzn  10036  zq  10041  icoshftf1o  10409  iccf1o  10423  fzen  10463  fzneuz  10524  4fvwrd4  10563  qltnle  10694  flqeqceilz  10775  modq0  10786  modqmuladdnn0  10825  addmodlteq  10855  nn0ennn  10890  uzennn  10893  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  seq3f1olemstep  10971  exp3val  10998  qsqeqor  11107  hashfacen  11305  hashf1lem1  11306  wrd2ind  11516  cjreb  11652  caucvgrelemrec  11766  minmax  12019  xrnegiso  12052  xrnegcon1d  12054  xrminmax  12055  pwm1geoserap1  12299  dvdsval2  12581  dvdsabseq  12638  dvdsflip  12642  odd2np1  12664  oddm1even  12666  sqoddm1div8z  12677  m1exp1  12692  divalgb  12716  modremain  12720  zeqzmulgcd  12771  dfgcd2  12815  divgcdcoprm0  12903  prm2orodd  12928  hashdvds  13027  oddprmdvds  13161  ballotfilemsima  13316  oddennn  13340  evenennn  13341  gzsumval2  13772  grpid  13902  grpinvcnv  13931  grplmulf1o  13937  grpsubeq0  13949  grpsubadd  13951  grplactcnv  13965  isnsg4  14073  eqg0el  14090  conjghm  14137  conjnmzb  14141  cntzrec  14168  dvdsr02  14520  01eq0ring  14604  rmodislmodlem  14795  rspsn  14979  zndvds  15092  znleval  15096  psrbagconf1o  15177  psr1clfi  15207  toponsspwpwg  15265  dmtopon  15266  hmeoimaf1o  15557  txhmeo  15562  limcmpted  15906  ioocosf1o  16099  fsumdvdsmul  16302  gausslemma2dlem0i  16398  lgseisenlem2  16412  lgsquadlem2  16419  2lgslem1c  16431  2lgsoddprmlem2  16447  2lgsoddprm  16454  uspgredgiedg  16641  uspgriedgedg  16642  uspgr2wlkeq  16828  wlk0prc  16835  wlklenvclwlk  16836  eupth2lem2dc  16922  bj-peano4  17203  pwle2  17250  subctctexmid  17252  pw1nct  17255  rabid1o  17256  stnot  17261  exmidsbthrlem  17290  iooref1o  17306  iswomni0  17325