Theorem eqcom 2240

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

This proof depends on syntax axioms:   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqcoms  2241  eqcomi  2242  neqcomd  2243  eqcomd  2244  eqeq2  2248  eqtr2  2257  eqtr3  2258  abeq1  2348  eqabcbw  2376  eqabcb  2377  nesym  2465  pm13.181  2502  necom  2504  gencbvex  2869  gencbval  2871  clel5  2963  eqsbc2  3112  dfss  3234  dfss5  3436  rabrsndc  3779  preqr1g  3891  preqr1  3893  invdisj  4123  opthg2  4379  copsex4g  4387  opcom  4391  opeqsn  4393  opeqpr  4394  reusv3  4606  suc11g  4704  opthprc  4826  elxp3  4829  relop  4930  dmopab3  4994  rncoeq  5056  restidsing  5119  dfrel4v  5239  dmsnm  5253  iota1  5352  sniota  5368  dffn5im  5748  fvelrnb  5750  dfimafn2  5752  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fneqeql  5817  rexrn  5845  ralrn  5846  elrnrexdmb  5848  dffo4  5856  ftpg  5899  fconstfvm  5933  dfimafnf  5955  foima2  5957  rexima  5960  ralima  5961  dff13  5974  f1eqcocnv  5997  riotaeqimp  6063  eusvobj2  6071  f1ocnvfv3  6074  oprabid  6117  eloprabga  6175  ovelimab  6240  dfoprab3  6425  f1o2ndf1  6464  cnvoprab  6470  brtpos2  6522  tpossym  6547  frecsuclem  6677  nntri3or  6766  erth2  6854  brecop  6899  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  xpcomco  7124  mapen  7146  nneneq  7158  supelti  7343  djuf1olem  7394  eldju  7409  omp1eomlem  7435  nninfwlporlemd  7513  exmidontriimlem3  7580  ordpipqqs  7742  addcanprg  7984  ltsrprg  8115  caucvgsrlemcl  8157  caucvgsrlemfv  8159  elreal  8196  ltresr  8207  axcaucvglemcl  8263  axcaucvglemval  8265  addsubeq4  8543  subcan2  8553  negcon1  8580  negcon2  8581  addid0  8701  addeq0  8705  divmulap2  9009  conjmulap  9062  rerecclap  9063  creur  9292  creui  9293  nndiv  9348  elznn0  9664  zltnle  9695  uzm1  9963  divfnzn  10031  zq  10036  icoshftf1o  10404  iccf1o  10418  fzen  10458  fzneuz  10519  4fvwrd4  10558  qltnle  10689  flqeqceilz  10770  modq0  10781  modqmuladdnn0  10820  addmodlteq  10850  nn0ennn  10885  uzennn  10888  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  seq3f1olemstep  10966  exp3val  10993  qsqeqor  11102  hashfacen  11300  hashf1lem1  11301  wrd2ind  11511  cjreb  11647  caucvgrelemrec  11761  minmax  12014  xrnegiso  12047  xrnegcon1d  12049  xrminmax  12050  pwm1geoserap1  12294  dvdsval2  12576  dvdsabseq  12633  dvdsflip  12637  odd2np1  12659  oddm1even  12661  sqoddm1div8z  12672  m1exp1  12687  divalgb  12711  modremain  12715  zeqzmulgcd  12766  dfgcd2  12810  divgcdcoprm0  12898  prm2orodd  12923  hashdvds  13022  oddprmdvds  13156  ballotfilemsima  13311  oddennn  13335  evenennn  13336  gzsumval2  13767  grpid  13897  grpinvcnv  13926  grplmulf1o  13932  grpsubeq0  13944  grpsubadd  13946  grplactcnv  13960  isnsg4  14068  eqg0el  14085  conjghm  14132  conjnmzb  14136  cntzrec  14163  dvdsr02  14496  01eq0ring  14580  rmodislmodlem  14771  rspsn  14955  zndvds  15068  znleval  15072  psrbagconf1o  15149  psr1clfi  15170  toponsspwpwg  15214  dmtopon  15215  hmeoimaf1o  15506  txhmeo  15511  limcmpted  15855  ioocosf1o  16047  fsumdvdsmul  16246  gausslemma2dlem0i  16342  lgseisenlem2  16356  lgsquadlem2  16363  2lgslem1c  16375  2lgsoddprmlem2  16391  2lgsoddprm  16398  uspgredgiedg  16585  uspgriedgedg  16586  uspgr2wlkeq  16772  wlk0prc  16779  wlklenvclwlk  16780  eupth2lem2dc  16866  bj-peano4  17147  pwle2  17194  subctctexmid  17196  pw1nct  17199  rabid1o  17200  stnot  17205  exmidsbthrlem  17233  iooref1o  17249  iswomni0  17268