Theorem eqcom 2172

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 1463	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2164	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2164	. 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 1346   = wceq 1348   e. wcel 2141

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 1440  ax-gen 1442  ax-ext 2152

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

This theorem is referenced by:  eqcoms  2173  eqcomi  2174  neqcomd  2175  eqcomd  2176  eqeq2  2180  eqtr2  2189  eqtr3  2190  abeq1  2280  nesym  2385  pm13.181  2422  necom  2424  gencbvex  2776  gencbval  2778  clel5  2867  eqsbc2  3015  dfss  3135  dfss5  3332  rabrsndc  3651  preqr1g  3753  preqr1  3755  invdisj  3983  opthg2  4224  copsex4g  4232  opcom  4235  opeqsn  4237  opeqpr  4238  reusv3  4445  suc11g  4541  opthprc  4662  elxp3  4665  relop  4761  dmopab3  4824  rncoeq  4884  dfrel4v  5062  dmsnm  5076  iota1  5174  sniota  5189  dffn5im  5542  fvelrnb  5544  dfimafn2  5546  funimass4  5547  fnsnfv  5555  dmfco  5564  fndmdif  5601  fneqeql  5604  rexrn  5633  ralrn  5634  elrnrexdmb  5636  dffo4  5644  ftpg  5680  fconstfvm  5714  foima2  5731  rexima  5734  ralima  5735  dff13  5747  f1eqcocnv  5770  eusvobj2  5839  f1ocnvfv3  5842  oprabid  5885  eloprabga  5940  ovelimab  6003  dfoprab3  6170  f1o2ndf1  6207  cnvoprab  6213  brtpos2  6230  tpossym  6255  frecsuclem  6385  nntri3or  6472  erth2  6558  brecop  6603  erovlem  6605  ecopovsym  6609  ecopovsymg  6612  xpcomco  6804  mapen  6824  nneneq  6835  supelti  6979  djuf1olem  7030  eldju  7045  omp1eomlem  7071  nninfwlporlemd  7148  exmidontriimlem3  7200  ordpipqqs  7336  addcanprg  7578  ltsrprg  7709  caucvgsrlemcl  7751  caucvgsrlemfv  7753  elreal  7790  ltresr  7801  axcaucvglemcl  7857  axcaucvglemval  7859  addsubeq4  8134  subcan2  8144  negcon1  8171  negcon2  8172  addid0  8292  divmulap2  8593  conjmulap  8646  rerecclap  8647  creur  8875  creui  8876  nndiv  8919  elznn0  9227  zltnle  9258  uzm1  9517  divfnzn  9580  zq  9585  icoshftf1o  9948  iccf1o  9961  fzen  9999  fzneuz  10057  4fvwrd4  10096  qltnle  10202  flqeqceilz  10274  modq0  10285  modqmuladdnn0  10324  addmodlteq  10354  nn0ennn  10389  uzennn  10392  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  seq3f1olemstep  10457  exp3val  10478  qsqeqor  10586  hashfacen  10771  cjreb  10830  caucvgrelemrec  10943  minmax  11193  xrnegiso  11225  xrnegcon1d  11227  xrminmax  11228  pwm1geoserap1  11471  dvdsval2  11752  dvdsabseq  11807  dvdsflip  11811  odd2np1  11832  oddm1even  11834  sqoddm1div8z  11845  m1exp1  11860  divalgb  11884  modremain  11888  zeqzmulgcd  11925  dfgcd2  11969  divgcdcoprm0  12055  prm2orodd  12080  hashdvds  12175  oddprmdvds  12306  oddennn  12347  evenennn  12348  grpid  12742  grpinvcnv  12767  toponsspwpwg  12814  dmtopon  12815  hmeoimaf1o  13108  txhmeo  13113  limcmpted  13426  ioocosf1o  13569  bj-peano4  13990  pwle2  14031  subctctexmid  14034  pw1nct  14036  exmidsbthrlem  14054  iooref1o  14066  iswomni0  14083