Theorem eqcom 2233

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 140	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1519	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2225	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2225	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 212	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 105   A.wal 1396   = wceq 1398   e. wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqcoms  2234  eqcomi  2235  neqcomd  2236  eqcomd  2237  eqeq2  2241  eqtr2  2250  eqtr3  2251  abeq1  2341  nesym  2448  pm13.181  2485  necom  2487  gencbvex  2851  gencbval  2853  clel5  2944  eqsbc2  3093  dfss  3215  dfss5  3414  rabrsndc  3743  preqr1g  3854  preqr1  3856  invdisj  4086  opthg2  4337  copsex4g  4345  opcom  4349  opeqsn  4351  opeqpr  4352  reusv3  4563  suc11g  4661  opthprc  4783  elxp3  4786  relop  4886  dmopab3  4950  rncoeq  5012  restidsing  5075  dfrel4v  5195  dmsnm  5209  iota1  5308  sniota  5324  dffn5im  5700  fvelrnb  5702  dfimafn2  5704  funimass4  5705  fnsnfv  5714  dmfco  5723  fndmdif  5761  fneqeql  5764  rexrn  5792  ralrn  5793  elrnrexdmb  5795  dffo4  5803  ftpg  5846  fconstfvm  5880  foima2  5902  rexima  5905  ralima  5906  dff13  5919  f1eqcocnv  5942  riotaeqimp  6006  eusvobj2  6014  f1ocnvfv3  6017  oprabid  6060  eloprabga  6118  ovelimab  6183  dfoprab3  6363  f1o2ndf1  6402  cnvoprab  6408  brtpos2  6460  tpossym  6485  frecsuclem  6615  nntri3or  6704  erth2  6792  brecop  6837  erovlem  6839  ecopovsym  6843  ecopovsymg  6846  xpcomco  7053  mapen  7075  nneneq  7086  supelti  7261  djuf1olem  7312  eldju  7327  omp1eomlem  7353  nninfwlporlemd  7431  exmidontriimlem3  7498  ordpipqqs  7654  addcanprg  7896  ltsrprg  8027  caucvgsrlemcl  8069  caucvgsrlemfv  8071  elreal  8108  ltresr  8119  axcaucvglemcl  8175  axcaucvglemval  8177  addsubeq4  8453  subcan2  8463  negcon1  8490  negcon2  8491  addid0  8611  divmulap2  8915  conjmulap  8968  rerecclap  8969  creur  9198  creui  9199  nndiv  9243  elznn0  9555  zltnle  9586  uzm1  9848  divfnzn  9916  zq  9921  icoshftf1o  10287  iccf1o  10301  fzen  10340  fzneuz  10398  4fvwrd4  10437  qltnle  10566  flqeqceilz  10643  modq0  10654  modqmuladdnn0  10693  addmodlteq  10723  nn0ennn  10758  uzennn  10761  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  seq3f1olemstep  10839  exp3val  10866  qsqeqor  10975  hashfacen  11163  wrd2ind  11370  cjreb  11506  caucvgrelemrec  11619  minmax  11870  xrnegiso  11902  xrnegcon1d  11904  xrminmax  11905  pwm1geoserap1  12149  dvdsval2  12431  dvdsabseq  12488  dvdsflip  12492  odd2np1  12514  oddm1even  12516  sqoddm1div8z  12527  m1exp1  12542  divalgb  12566  modremain  12570  zeqzmulgcd  12621  dfgcd2  12665  divgcdcoprm0  12753  prm2orodd  12778  hashdvds  12873  oddprmdvds  13007  oddennn  13093  evenennn  13094  gsumval2  13560  grpid  13702  grpinvcnv  13731  grplmulf1o  13737  grpsubeq0  13749  grpsubadd  13751  grplactcnv  13765  isnsg4  13879  eqg0el  13896  conjghm  13943  conjnmzb  13947  dvdsr02  14200  01eq0ring  14284  rmodislmodlem  14446  rspsn  14630  zndvds  14745  znleval  14749  psrbagconf1o  14774  psr1clfi  14789  toponsspwpwg  14833  dmtopon  14834  hmeoimaf1o  15125  txhmeo  15130  limcmpted  15474  ioocosf1o  15665  fsumdvdsmul  15805  gausslemma2dlem0i  15876  lgseisenlem2  15890  lgsquadlem2  15897  2lgslem1c  15909  2lgsoddprmlem2  15925  2lgsoddprm  15932  uspgredgiedg  16119  uspgriedgedg  16120  uspgr2wlkeq  16306  wlk0prc  16313  wlklenvclwlk  16314  eupth2lem2dc  16400  bj-peano4  16671  pwle2  16720  subctctexmid  16722  pw1nct  16725  exmidsbthrlem  16750  iooref1o  16766  iswomni0  16784