Theorem eqcom 2355

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 191	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	albii 1566	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 2347	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 2347	. 2 |- (B = A <-> A.x(x e. B <-> x e. A))
5	2, 3, 4	3bitr4i 268	1 |- (A = B <-> B = A)

Syntax hints:   <-> wb 176  A.wal 1540   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-cleq 2346

This theorem is referenced by:  eqcoms  2356  eqcomi  2357  eqcomd  2358  eqeq2  2362  eqtr2  2371  eqtr3  2372  abeq1  2459  pm13.181  2589  necom  2597  gencbvex  2901  reu7  3031  eqsbc3r  3103  dfss  3260  sspsstri  3371  dfss5  3461  disj4  3599  ssnelpss  3613  preqr1  4124  snelpw1  4146  0nel1c  4159  eluni1g  4172  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opksnelsik  4265  iota1  4353  sniota  4369  0nelsuc  4400  nndisjeq  4429  preaddccan2lem1  4454  0cnelphi  4597  copsex4g  4610  opeqexb  4620  br1stg  4730  setconslem1  4731  opelxp  4811  elxp3  4831  brswap2  4860  dmopab3  4917  rncoeq  4975  xpcan  5057  xpcan2  5058  dmsnn0  5064  dffn5  5363  fnrnfv  5364  fvelrnb  5365  dfimafn2  5367  funimass4  5368  fnsnfv  5373  dmfco  5381  fnasrn  5417  dffo4  5423  fconstfv  5456  fvclss  5462  funiunfv  5467  dff13  5471  isomin  5496  f1oiso  5499  opbr1st  5501  opbr2nd  5502  oprabid  5550  eloprabga  5578  ovelimab  5610  brsnsi  5773  brsnsi1  5775  brsnsi2  5776  brco1st  5777  brco2nd  5778  txpcofun  5803  otsnelsi3  5805  brcupg  5814  fnsex  5832  qrpprod  5836  dmpprod  5840  fnpprod  5843  brcrossg  5848  pw1fnex  5852  brpw1fn  5854  dfnnc3  5885  antisymex  5912  erth2  5969  qsid  5990  mapexi  6003  xpassenlem  6056  xpassen  6057  enmap2lem1  6063  enmap2lem3  6065  enmap1lem1  6069  nenpw1pwlem1  6084  ncseqnc  6128  leltctr  6212  taddc  6229  letc  6231  ce0lenc1  6239  brtcfn  6246  ncfin  6247  csucex  6259  addccan2nclem1  6263  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  nnc3n3p2  6279  spacvallem1  6281  nchoicelem1  6289  nchoicelem2  6290  nchoicelem16  6304