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  6588  ltsrprg  6635  elreal  6687  ltresr  6696  addsubeq4  6983  subcan2  6992  negcon1  7019  negcon2  7020  divmulap2  7397  conjmulap  7447  rerecclap  7448  creur  7652  creui  7653  nndiv  7695  elznn0  7996  zltnle  8027  uzm1  8239  divfnzn  8292  zq  8297  icoshftf1o  8589  iccf1o  8602  fzen  8637  fzneuz  8693  4fvwrd4  8727  nn0ennn  8850  cjreb  9054  bj-peano4  9343