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  2460  pm13.181  2590  necom  2598  gencbvex  2902  reu7  3032  eqsbc2  3104  dfss  3261  sspsstri  3372  dfss5  3462  disj4  3600  ssnelpss  3614  preqr1  4125  snelpw1  4147  0nel1c  4160  eluni1g  4173  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opksnelsik  4266  iota1  4354  sniota  4370  0nelsuc  4401  nndisjeq  4430  preaddccan2lem1  4455  0cnelphi  4598  copsex4g  4611  opeqexb  4621  br1stg  4731  setconslem1  4732  opelxp  4812  elxp3  4832  brswap2  4861  dmopab3  4918  rncoeq  4976  xpcan  5058  xpcan2  5059  dmsnn0  5065  dffn5  5364  fnrnfv  5365  fvelrnb  5366  dfimafn2  5368  funimass4  5369  fnsnfv  5374  dmfco  5382  fnasrn  5418  dffo4  5424  fconstfv  5457  fvclss  5463  funiunfv  5468  dff13  5472  isomin  5497  f1oiso  5500  opbr1st  5502  opbr2nd  5503  oprabid  5551  eloprabga  5579  ovelimab  5611  brsnsi  5774  brsnsi1  5776  brsnsi2  5777  brco1st  5778  brco2nd  5779  txpcofun  5804  otsnelsi3  5806  brcupg  5815  fnsex  5833  qrpprod  5837  dmpprod  5841  fnpprod  5844  brcrossg  5849  pw1fnex  5853  brpw1fn  5855  dfnnc3  5886  antisymex  5913  erth2  5970  qsid  5991  mapexi  6004  xpassenlem  6057  xpassen  6058  enmap2lem1  6064  enmap2lem3  6066  enmap1lem1  6070  nenpw1pwlem1  6085  ncseqnc  6129  leltctr  6213  taddc  6230  letc  6232  ce0lenc1  6240  brtcfn  6247  ncfin  6248  csucex  6260  addccan2nclem1  6264  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  nnc3n3p2  6280  spacvallem1  6282  nchoicelem1  6290  nchoicelem2  6291  nchoicelem16  6305