Theorem eqcom 2236

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 2228	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2228	. 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 2205

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 2216

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

This theorem is referenced by:  eqcoms  2237  eqcomi  2238  neqcomd  2239  eqcomd  2240  eqeq2  2244  eqtr2  2253  eqtr3  2254  abeq1  2344  eqabcb  2371  nesym  2459  pm13.181  2496  necom  2498  gencbvex  2863  gencbval  2865  clel5  2957  eqsbc2  3106  dfss  3228  dfss5  3430  rabrsndc  3764  preqr1g  3875  preqr1  3877  invdisj  4107  opthg2  4360  copsex4g  4368  opcom  4372  opeqsn  4374  opeqpr  4375  reusv3  4586  suc11g  4684  opthprc  4806  elxp3  4809  relop  4910  dmopab3  4974  rncoeq  5036  restidsing  5099  dfrel4v  5219  dmsnm  5233  iota1  5332  sniota  5348  dffn5im  5727  fvelrnb  5729  dfimafn2  5731  funimass4  5732  fnsnfv  5741  dmfco  5750  fndmdif  5788  fneqeql  5791  rexrn  5819  ralrn  5820  elrnrexdmb  5822  dffo4  5830  ftpg  5873  fconstfvm  5907  dfimafnf  5928  foima2  5930  rexima  5933  ralima  5934  dff13  5947  f1eqcocnv  5970  riotaeqimp  6036  eusvobj2  6044  f1ocnvfv3  6047  oprabid  6090  eloprabga  6148  ovelimab  6213  dfoprab3  6398  f1o2ndf1  6437  cnvoprab  6443  brtpos2  6495  tpossym  6520  frecsuclem  6650  nntri3or  6739  erth2  6827  brecop  6872  erovlem  6874  ecopovsym  6878  ecopovsymg  6881  xpcomco  7090  mapen  7112  nneneq  7124  supelti  7306  djuf1olem  7357  eldju  7372  omp1eomlem  7398  nninfwlporlemd  7476  exmidontriimlem3  7543  ordpipqqs  7705  addcanprg  7947  ltsrprg  8078  caucvgsrlemcl  8120  caucvgsrlemfv  8122  elreal  8159  ltresr  8170  axcaucvglemcl  8226  axcaucvglemval  8228  addsubeq4  8504  subcan2  8514  negcon1  8541  negcon2  8542  addid0  8662  addeq0  8666  divmulap2  8967  conjmulap  9020  rerecclap  9021  creur  9250  creui  9251  nndiv  9295  elznn0  9609  zltnle  9640  uzm1  9903  divfnzn  9971  zq  9976  icoshftf1o  10343  iccf1o  10357  fzen  10397  fzneuz  10457  4fvwrd4  10496  qltnle  10627  flqeqceilz  10704  modq0  10715  modqmuladdnn0  10754  addmodlteq  10784  nn0ennn  10819  uzennn  10822  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  seq3f1olemstep  10900  exp3val  10927  qsqeqor  11036  hashfacen  11233  wrd2ind  11440  cjreb  11576  caucvgrelemrec  11689  minmax  11940  xrnegiso  11972  xrnegcon1d  11974  xrminmax  11975  pwm1geoserap1  12219  dvdsval2  12501  dvdsabseq  12558  dvdsflip  12562  odd2np1  12584  oddm1even  12586  sqoddm1div8z  12597  m1exp1  12612  divalgb  12636  modremain  12640  zeqzmulgcd  12691  dfgcd2  12735  divgcdcoprm0  12823  prm2orodd  12848  hashdvds  12943  oddprmdvds  13077  ballotfilemsima  13203  oddennn  13227  evenennn  13228  gsumval2  13660  grpid  13794  grpinvcnv  13823  grplmulf1o  13829  grpsubeq0  13841  grpsubadd  13843  grplactcnv  13857  isnsg4  13965  eqg0el  13982  conjghm  14029  conjnmzb  14033  dvdsr02  14350  01eq0ring  14434  rmodislmodlem  14624  rspsn  14808  zndvds  14923  znleval  14927  psrbagconf1o  14954  psr1clfi  14969  toponsspwpwg  15013  dmtopon  15014  hmeoimaf1o  15305  txhmeo  15310  limcmpted  15654  ioocosf1o  15845  fsumdvdsmul  15985  gausslemma2dlem0i  16056  lgseisenlem2  16070  lgsquadlem2  16077  2lgslem1c  16089  2lgsoddprmlem2  16105  2lgsoddprm  16112  uspgredgiedg  16299  uspgriedgedg  16300  uspgr2wlkeq  16486  wlk0prc  16493  wlklenvclwlk  16494  eupth2lem2dc  16580  bj-peano4  16851  pwle2  16898  subctctexmid  16900  pw1nct  16903  exmidsbthrlem  16928  iooref1o  16944  iswomni0  16962