Theorem eqcom 2207

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 1493	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2199	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2199	. 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 1371   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ext 2187

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

This theorem is referenced by:  eqcoms  2208  eqcomi  2209  neqcomd  2210  eqcomd  2211  eqeq2  2215  eqtr2  2224  eqtr3  2225  abeq1  2315  nesym  2421  pm13.181  2458  necom  2460  gencbvex  2819  gencbval  2821  clel5  2910  eqsbc2  3059  dfss  3180  dfss5  3378  rabrsndc  3701  preqr1g  3807  preqr1  3809  invdisj  4038  opthg2  4283  copsex4g  4291  opcom  4295  opeqsn  4297  opeqpr  4298  reusv3  4507  suc11g  4605  opthprc  4726  elxp3  4729  relop  4828  dmopab3  4891  rncoeq  4952  restidsing  5015  dfrel4v  5134  dmsnm  5148  iota1  5246  sniota  5262  dffn5im  5624  fvelrnb  5626  dfimafn2  5628  funimass4  5629  fnsnfv  5638  dmfco  5647  fndmdif  5685  fneqeql  5688  rexrn  5717  ralrn  5718  elrnrexdmb  5720  dffo4  5728  ftpg  5768  fconstfvm  5802  foima2  5820  rexima  5823  ralima  5824  dff13  5837  f1eqcocnv  5860  eusvobj2  5930  f1ocnvfv3  5933  oprabid  5976  eloprabga  6032  ovelimab  6097  dfoprab3  6277  f1o2ndf1  6314  cnvoprab  6320  brtpos2  6337  tpossym  6362  frecsuclem  6492  nntri3or  6579  erth2  6667  brecop  6712  erovlem  6714  ecopovsym  6718  ecopovsymg  6721  xpcomco  6921  mapen  6943  nneneq  6954  supelti  7104  djuf1olem  7155  eldju  7170  omp1eomlem  7196  nninfwlporlemd  7274  exmidontriimlem3  7335  ordpipqqs  7487  addcanprg  7729  ltsrprg  7860  caucvgsrlemcl  7902  caucvgsrlemfv  7904  elreal  7941  ltresr  7952  axcaucvglemcl  8008  axcaucvglemval  8010  addsubeq4  8287  subcan2  8297  negcon1  8324  negcon2  8325  addid0  8445  divmulap2  8749  conjmulap  8802  rerecclap  8803  creur  9032  creui  9033  nndiv  9077  elznn0  9387  zltnle  9418  uzm1  9679  divfnzn  9742  zq  9747  icoshftf1o  10113  iccf1o  10126  fzen  10165  fzneuz  10223  4fvwrd4  10262  qltnle  10386  flqeqceilz  10463  modq0  10474  modqmuladdnn0  10513  addmodlteq  10543  nn0ennn  10578  uzennn  10581  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  seq3f1olemstep  10659  exp3val  10686  qsqeqor  10795  hashfacen  10981  cjreb  11177  caucvgrelemrec  11290  minmax  11541  xrnegiso  11573  xrnegcon1d  11575  xrminmax  11576  pwm1geoserap1  11819  dvdsval2  12101  dvdsabseq  12158  dvdsflip  12162  odd2np1  12184  oddm1even  12186  sqoddm1div8z  12197  m1exp1  12212  divalgb  12236  modremain  12240  zeqzmulgcd  12291  dfgcd2  12335  divgcdcoprm0  12423  prm2orodd  12448  hashdvds  12543  oddprmdvds  12677  oddennn  12763  evenennn  12764  gsumval2  13229  grpid  13371  grpinvcnv  13400  grplmulf1o  13406  grpsubeq0  13418  grpsubadd  13420  grplactcnv  13434  isnsg4  13548  eqg0el  13565  conjghm  13612  conjnmzb  13616  dvdsr02  13867  01eq0ring  13951  rmodislmodlem  14112  rspsn  14296  zndvds  14411  znleval  14415  psr1clfi  14450  toponsspwpwg  14494  dmtopon  14495  hmeoimaf1o  14786  txhmeo  14791  limcmpted  15135  ioocosf1o  15326  fsumdvdsmul  15463  gausslemma2dlem0i  15534  lgseisenlem2  15548  lgsquadlem2  15555  2lgslem1c  15567  2lgsoddprmlem2  15583  2lgsoddprm  15590  bj-peano4  15891  pwle2  15935  subctctexmid  15937  pw1nct  15940  exmidsbthrlem  15961  iooref1o  15973  iswomni0  15990