Theorem eqcom 2039

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqcom	⊢ (A = B ↔ B = A)

Proof of Theorem eqcom

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 128	. . 3 ⊢ ((x ∈ A ↔ x ∈ B) ↔ (x ∈ B ↔ x ∈ A))
2	1	albii 1356	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ ∀x(x ∈ B ↔ x ∈ A))
3		dfcleq 2031	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4		dfcleq 2031	. 2 ⊢ (B = A ↔ ∀x(x ∈ B ↔ x ∈ A))
5	2, 3, 4	3bitr4i 201	1 ⊢ (A = B ↔ B = A)

Syntax hints:   ↔ wb 98  ∀wal 1240   = wceq 1242   ∈ wcel 1390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqcoms  2040  eqcomi  2041  eqcomd  2042  eqeq2  2046  eqtr2  2055  eqtr3  2056  abeq1  2144  nesym  2244  pm13.181  2281  necom  2283  gencbvex  2594  gencbval  2596  eqsbc3r  2813  dfss  2926  dfss5  3136  disj4im  3270  ssnelpss  3283  rabrsndc  3429  preqr1g  3528  preqr1  3530  invdisj  3750  opthg2  3967  copsex4g  3975  opcom  3978  opeqsn  3980  opeqpr  3981  reusv3  4158  suc11g  4235  dtruex  4237  opthprc  4334  elxp3  4337  relop  4429  dmopab3  4491  rncoeq  4548  dfrel4v  4715  dmsnm  4729  iota1  4824  sniota  4837  dffn5im  5162  fvelrnb  5164  dfimafn2  5166  funimass4  5167  fnsnfv  5175  dmfco  5184  fndmdif  5215  fneqeql  5218  rexrn  5247  ralrn  5248  elrnrexdmb  5250  dffo4  5258  ftpg  5290  fconstfvm  5322  rexima  5337  ralima  5338  dff13  5350  f1eqcocnv  5374  eusvobj2  5441  f1ocnvfv3  5444  oprabid  5480  eloprabga  5533  ovelimab  5593  dfoprab3  5759  f1o2ndf1  5791  brtpos2  5807  tpossym  5832  frecsuclem3  5929  nntri3or  6011  erth2  6087  brecop  6132  erovlem  6134  ecopovsym  6138  ecopovsymg  6141  xpcomco  6236  ordpipqqs  6358  addcanprg  6590  ltsrprg  6675  elreal  6727  ltresr  6736  addsubeq4  7023  subcan2  7032  negcon1  7059  negcon2  7060  divmulap2  7437  conjmulap  7487  rerecclap  7488  creur  7692  creui  7693  nndiv  7735  elznn0  8036  zltnle  8067  uzm1  8279  divfnzn  8332  zq  8337  icoshftf1o  8629  iccf1o  8642  fzen  8677  fzneuz  8733  4fvwrd4  8767  nn0ennn  8890  cjreb  9094  bj-peano4  9415