Theorem eqcom 2191

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 1481	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2183	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2183	. 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 1362   = wceq 1364   e. wcel 2160

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 1458  ax-gen 1460  ax-ext 2171

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

This theorem is referenced by:  eqcoms  2192  eqcomi  2193  neqcomd  2194  eqcomd  2195  eqeq2  2199  eqtr2  2208  eqtr3  2209  abeq1  2299  nesym  2405  pm13.181  2442  necom  2444  gencbvex  2798  gencbval  2800  clel5  2889  eqsbc2  3038  dfss  3158  dfss5  3355  rabrsndc  3675  preqr1g  3781  preqr1  3783  invdisj  4012  opthg2  4257  copsex4g  4265  opcom  4268  opeqsn  4270  opeqpr  4271  reusv3  4478  suc11g  4574  opthprc  4695  elxp3  4698  relop  4795  dmopab3  4858  rncoeq  4918  restidsing  4981  dfrel4v  5098  dmsnm  5112  iota1  5210  sniota  5226  dffn5im  5582  fvelrnb  5584  dfimafn2  5586  funimass4  5587  fnsnfv  5596  dmfco  5605  fndmdif  5642  fneqeql  5645  rexrn  5674  ralrn  5675  elrnrexdmb  5677  dffo4  5685  ftpg  5721  fconstfvm  5755  foima2  5773  rexima  5776  ralima  5777  dff13  5790  f1eqcocnv  5813  eusvobj2  5883  f1ocnvfv3  5886  oprabid  5929  eloprabga  5984  ovelimab  6048  dfoprab3  6217  f1o2ndf1  6254  cnvoprab  6260  brtpos2  6277  tpossym  6302  frecsuclem  6432  nntri3or  6519  erth2  6607  brecop  6652  erovlem  6654  ecopovsym  6658  ecopovsymg  6661  xpcomco  6853  mapen  6875  nneneq  6886  supelti  7032  djuf1olem  7083  eldju  7098  omp1eomlem  7124  nninfwlporlemd  7201  exmidontriimlem3  7253  ordpipqqs  7404  addcanprg  7646  ltsrprg  7777  caucvgsrlemcl  7819  caucvgsrlemfv  7821  elreal  7858  ltresr  7869  axcaucvglemcl  7925  axcaucvglemval  7927  addsubeq4  8203  subcan2  8213  negcon1  8240  negcon2  8241  addid0  8361  divmulap2  8664  conjmulap  8717  rerecclap  8718  creur  8947  creui  8948  nndiv  8991  elznn0  9299  zltnle  9330  uzm1  9590  divfnzn  9653  zq  9658  icoshftf1o  10023  iccf1o  10036  fzen  10075  fzneuz  10133  4fvwrd4  10172  qltnle  10278  flqeqceilz  10351  modq0  10362  modqmuladdnn0  10401  addmodlteq  10431  nn0ennn  10466  uzennn  10469  iseqf1olemqcl  10519  iseqf1olemnab  10521  iseqf1olemab  10522  seq3f1olemstep  10534  exp3val  10556  qsqeqor  10665  hashfacen  10851  cjreb  10910  caucvgrelemrec  11023  minmax  11273  xrnegiso  11305  xrnegcon1d  11307  xrminmax  11308  pwm1geoserap1  11551  dvdsval2  11832  dvdsabseq  11888  dvdsflip  11892  odd2np1  11913  oddm1even  11915  sqoddm1div8z  11926  m1exp1  11941  divalgb  11965  modremain  11969  zeqzmulgcd  12006  dfgcd2  12050  divgcdcoprm0  12136  prm2orodd  12161  hashdvds  12256  oddprmdvds  12389  oddennn  12446  evenennn  12447  gsumval2  12875  grpid  12998  grpinvcnv  13027  grplmulf1o  13033  grpsubeq0  13045  grpsubadd  13047  grplactcnv  13061  isnsg4  13168  eqg0el  13185  conjghm  13232  conjnmzb  13236  dvdsr02  13472  01eq0ring  13553  rmodislmodlem  13683  toponsspwpwg  13999  dmtopon  14000  hmeoimaf1o  14291  txhmeo  14296  limcmpted  14609  ioocosf1o  14752  lgseisenlem2  14929  2lgsoddprmlem2  14932  bj-peano4  15185  pwle2  15227  subctctexmid  15229  pw1nct  15231  exmidsbthrlem  15249  iooref1o  15261  iswomni0  15278