Theorem eqcom 2167

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 139	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1458	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2159	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2159	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 211	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 104   A.wal 1341   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqcoms  2168  eqcomi  2169  neqcomd  2170  eqcomd  2171  eqeq2  2175  eqtr2  2184  eqtr3  2185  abeq1  2276  nesym  2381  pm13.181  2418  necom  2420  gencbvex  2772  gencbval  2774  clel5  2863  eqsbc2  3011  dfss  3130  dfss5  3327  rabrsndc  3644  preqr1g  3746  preqr1  3748  invdisj  3976  opthg2  4217  copsex4g  4225  opcom  4228  opeqsn  4230  opeqpr  4231  reusv3  4438  suc11g  4534  opthprc  4655  elxp3  4658  relop  4754  dmopab3  4817  rncoeq  4877  dfrel4v  5055  dmsnm  5069  iota1  5167  sniota  5180  dffn5im  5532  fvelrnb  5534  dfimafn2  5536  funimass4  5537  fnsnfv  5545  dmfco  5554  fndmdif  5590  fneqeql  5593  rexrn  5622  ralrn  5623  elrnrexdmb  5625  dffo4  5633  ftpg  5669  fconstfvm  5703  foima2  5720  rexima  5723  ralima  5724  dff13  5736  f1eqcocnv  5759  eusvobj2  5828  f1ocnvfv3  5831  oprabid  5874  eloprabga  5929  ovelimab  5992  dfoprab3  6159  f1o2ndf1  6196  cnvoprab  6202  brtpos2  6219  tpossym  6244  frecsuclem  6374  nntri3or  6461  erth2  6546  brecop  6591  erovlem  6593  ecopovsym  6597  ecopovsymg  6600  xpcomco  6792  mapen  6812  nneneq  6823  supelti  6967  djuf1olem  7018  eldju  7033  omp1eomlem  7059  exmidontriimlem3  7179  ordpipqqs  7315  addcanprg  7557  ltsrprg  7688  caucvgsrlemcl  7730  caucvgsrlemfv  7732  elreal  7769  ltresr  7780  axcaucvglemcl  7836  axcaucvglemval  7838  addsubeq4  8113  subcan2  8123  negcon1  8150  negcon2  8151  addid0  8271  divmulap2  8572  conjmulap  8625  rerecclap  8626  creur  8854  creui  8855  nndiv  8898  elznn0  9206  zltnle  9237  uzm1  9496  divfnzn  9559  zq  9564  icoshftf1o  9927  iccf1o  9940  fzen  9978  fzneuz  10036  4fvwrd4  10075  qltnle  10181  flqeqceilz  10253  modq0  10264  modqmuladdnn0  10303  addmodlteq  10333  nn0ennn  10368  uzennn  10371  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemab  10424  seq3f1olemstep  10436  exp3val  10457  qsqeqor  10565  hashfacen  10749  cjreb  10808  caucvgrelemrec  10921  minmax  11171  xrnegiso  11203  xrnegcon1d  11205  xrminmax  11206  pwm1geoserap1  11449  dvdsval2  11730  dvdsabseq  11785  dvdsflip  11789  odd2np1  11810  oddm1even  11812  sqoddm1div8z  11823  m1exp1  11838  divalgb  11862  modremain  11866  zeqzmulgcd  11903  dfgcd2  11947  divgcdcoprm0  12033  prm2orodd  12058  hashdvds  12153  oddprmdvds  12284  oddennn  12325  evenennn  12326  toponsspwpwg  12660  dmtopon  12661  hmeoimaf1o  12954  txhmeo  12959  limcmpted  13272  ioocosf1o  13415  bj-peano4  13837  pwle2  13878  subctctexmid  13881  pw1nct  13883  exmidsbthrlem  13901  iooref1o  13913  iswomni0  13930