Theorem eqcom 2025

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 2017	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4		dfcleq 2017	. 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 1375

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 2005

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

This theorem is referenced by:  eqcoms  2026  eqcomi  2027  eqcomd  2028  eqeq2  2032  eqtr2  2041  eqtr3  2042  abeq1  2130  nesym  2227  pm13.181  2264  necom  2266  gencbvex  2576  gencbval  2578  eqsbc3r  2795  dfss  2908  dfss5  3118  disj4im  3252  ssnelpss  3265  rabrsndc  3411  preqr1g  3510  preqr1  3512  invdisj  3732  opthg2  3949  copsex4g  3957  opcom  3960  opeqsn  3962  opeqpr  3963  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  5737  f1o2ndf1  5769  brtpos2  5785  tpossym  5810  frec0g  5897  frecsuclem3  5901  nntri3or  5982  erth2  6056  brecop  6100  erovlem  6102  ecopovsym  6106  ecopovsymg  6109  ordpipqqs  6225  bj-peano4  6522