Theorem eqcom 2141

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 1446	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2133	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2133	. 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 1329   = wceq 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-ext 2121

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

This theorem is referenced by:  eqcoms  2142  eqcomi  2143  neqcomd  2144  eqcomd  2145  eqeq2  2149  eqtr2  2158  eqtr3  2159  abeq1  2249  nesym  2353  pm13.181  2390  necom  2392  gencbvex  2732  gencbval  2734  eqsbc3r  2969  dfss  3085  dfss5  3281  rabrsndc  3591  preqr1g  3693  preqr1  3695  invdisj  3923  opthg2  4161  copsex4g  4169  opcom  4172  opeqsn  4174  opeqpr  4175  reusv3  4381  suc11g  4472  opthprc  4590  elxp3  4593  relop  4689  dmopab3  4752  rncoeq  4812  dfrel4v  4990  dmsnm  5004  iota1  5102  sniota  5115  dffn5im  5467  fvelrnb  5469  dfimafn2  5471  funimass4  5472  fnsnfv  5480  dmfco  5489  fndmdif  5525  fneqeql  5528  rexrn  5557  ralrn  5558  elrnrexdmb  5560  dffo4  5568  ftpg  5604  fconstfvm  5638  foima2  5653  rexima  5656  ralima  5657  dff13  5669  f1eqcocnv  5692  eusvobj2  5760  f1ocnvfv3  5763  oprabid  5803  eloprabga  5858  ovelimab  5921  dfoprab3  6089  f1o2ndf1  6125  cnvoprab  6131  brtpos2  6148  tpossym  6173  frecsuclem  6303  nntri3or  6389  erth2  6474  brecop  6519  erovlem  6521  ecopovsym  6525  ecopovsymg  6528  xpcomco  6720  mapen  6740  nneneq  6751  supelti  6889  djuf1olem  6938  eldju  6953  omp1eomlem  6979  ordpipqqs  7182  addcanprg  7424  ltsrprg  7555  caucvgsrlemcl  7597  caucvgsrlemfv  7599  elreal  7636  ltresr  7647  axcaucvglemcl  7703  axcaucvglemval  7705  addsubeq4  7977  subcan2  7987  negcon1  8014  negcon2  8015  addid0  8135  divmulap2  8436  conjmulap  8489  rerecclap  8490  creur  8717  creui  8718  nndiv  8761  elznn0  9069  zltnle  9100  uzm1  9356  divfnzn  9413  zq  9418  icoshftf1o  9774  iccf1o  9787  fzen  9823  fzneuz  9881  4fvwrd4  9917  qltnle  10023  flqeqceilz  10091  modq0  10102  modqmuladdnn0  10141  addmodlteq  10171  nn0ennn  10206  uzennn  10209  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  seq3f1olemstep  10274  exp3val  10295  hashfacen  10579  cjreb  10638  caucvgrelemrec  10751  minmax  11001  xrnegiso  11031  xrnegcon1d  11033  xrminmax  11034  pwm1geoserap1  11277  dvdsval2  11496  dvdsabseq  11545  dvdsflip  11549  odd2np1  11570  oddm1even  11572  sqoddm1div8z  11583  m1exp1  11598  divalgb  11622  modremain  11626  zeqzmulgcd  11659  dfgcd2  11702  divgcdcoprm0  11782  prm2orodd  11807  hashdvds  11897  oddennn  11905  evenennn  11906  toponsspwpwg  12189  dmtopon  12190  hmeoimaf1o  12483  txhmeo  12488  limcmpted  12801  bj-peano4  13153  pwle2  13193  subctctexmid  13196  exmidsbthrlem  13217