Theorem eqcom 2024

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 1339	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ ∀x(x ∈ B ↔ x ∈ A))
3		dfcleq 2016	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4		dfcleq 2016	. 2 ⊢ (B = A ↔ ∀x(x ∈ B ↔ x ∈ A))
5	2, 3, 4	3bitr4i 201	1 ⊢ (A = B ↔ B = A)

Syntax hints:   ↔ wb 98  ∀wal 1226   = wceq 1228   ∈ wcel 1374

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 1316  ax-gen 1318  ax-ext 2004

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

This theorem is referenced by:  eqcoms  2025  eqcomi  2026  eqcomd  2027  eqeq2  2031  eqtr2  2040  eqtr3  2041  abeq1  2129  nesym  2226  pm13.181  2263  necom  2265  gencbvex  2575  gencbval  2577  eqsbc3r  2794  dfss  2907  dfss5  3117  disj4im  3251  ssnelpss  3264  rabrsndc  3410  preqr1g  3509  preqr1  3511  invdisj  3731  opthg2  3948  copsex4g  3956  opcom  3959  opeqsn  3961  opeqpr  3962  reusv3  4140  suc11g  4217  dtruex  4219  opthprc  4316  elxp3  4319  relop  4411  dmopab3  4473  rncoeq  4530  dfrel4v  4697  dmsnm  4711  iota1  4806  sniota  4819  dffn5im  5142  fvelrnb  5144  dfimafn2  5146  funimass4  5147  fnsnfv  5155  dmfco  5164  fndmdif  5195  fneqeql  5198  rexrn  5227  ralrn  5228  elrnrexdmb  5230  dffo4  5238  ftpg  5270  fconstfvm  5302  rexima  5317  ralima  5318  dff13  5330  f1eqcocnv  5354  eusvobj2  5420  f1ocnvfv3  5423  oprabid  5459  eloprabga  5512  ovelimab  5572  dfoprab3  5738  f1o2ndf1  5770  brtpos2  5786  tpossym  5811  frec0g  5900  frecsuclem3  5904  nntri3or  5985  erth2  6060  brecop  6105  erovlem  6107  ecopovsym  6111  ecopovsymg  6114  ordpipqqs  6231  addcanprg  6451  ltsrprg  6492  elreal  6539  ltresr  6548  bj-peano4  6856