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  4381  copsex4g  4389  opcom  4393  opeqsn  4395  opeqpr  4396  reusv3  4608  suc11g  4706  opthprc  4828  elxp3  4831  relop  4932  dmopab3  4996  rncoeq  5058  restidsing  5122  dfrel4v  5242  dmsnm  5256  iota1  5355  sniota  5371  dffn5im  5751  fvelrnb  5753  dfimafn2  5755  funimass4  5756  fnsnfv  5765  dmfco  5776  fndmdif  5817  fneqeql  5820  rexrn  5848  ralrn  5849  elrnrexdmb  5851  dffo4  5859  ftpg  5902  fconstfvm  5936  dfimafnf  5958  foima2  5960  rexima  5963  ralima  5964  dff13  5977  f1eqcocnv  6000  riotaeqimp  6066  eusvobj2  6074  f1ocnvfv3  6077  oprabid  6120  eloprabga  6178  ovelimab  6243  dfoprab3  6429  f1o2ndf1  6468  cnvoprab  6474  brtpos2  6526  tpossym  6551  frecsuclem  6681  nntri3or  6770  erth2  6858  brecop  6903  erovlem  6905  ecopovsym  6909  ecopovsymg  6912  xpcomco  7128  mapen  7150  nneneq  7162  supelti  7348  djuf1olem  7399  eldju  7414  omp1eomlem  7440  nninfwlporlemd  7518  exmidontriimlem3  7585  ordpipqqs  7747  addcanprg  7989  ltsrprg  8120  caucvgsrlemcl  8162  caucvgsrlemfv  8164  elreal  8201  ltresr  8212  axcaucvglemcl  8268  axcaucvglemval  8270  addsubeq4  8548  subcan2  8558  negcon1  8585  negcon2  8586  addid0  8706  addeq0  8710  divmulap2  9014  conjmulap  9067  rerecclap  9068  creur  9297  creui  9298  nndiv  9354  elznn0  9670  zltnle  9701  uzm1  9969  divfnzn  10037  zq  10042  icoshftf1o  10410  iccf1o  10424  fzen  10464  fzneuz  10525  4fvwrd4  10564  qltnle  10695  flqeqceilz  10776  modq0  10787  modqmuladdnn0  10826  addmodlteq  10856  nn0ennn  10891  uzennn  10894  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  seq3f1olemstep  10972  exp3val  10999  qsqeqor  11108  hashfacen  11306  hashf1lem1  11307  wrd2ind  11517  cjreb  11653  caucvgrelemrec  11767  minmax  12020  xrnegiso  12053  xrnegcon1d  12055  xrminmax  12056  pwm1geoserap1  12300  dvdsval2  12582  dvdsabseq  12639  dvdsflip  12643  odd2np1  12665  oddm1even  12667  sqoddm1div8z  12678  m1exp1  12693  divalgb  12717  modremain  12721  zeqzmulgcd  12772  dfgcd2  12816  divgcdcoprm0  12904  prm2orodd  12929  hashdvds  13028  oddprmdvds  13162  ballotfilemsima  13317  oddennn  13341  evenennn  13342  gzsumval2  13773  grpid  13903  grpinvcnv  13932  grplmulf1o  13938  grpsubeq0  13950  grpsubadd  13952  grplactcnv  13966  isnsg4  14074  eqg0el  14091  conjghm  14138  conjnmzb  14142  cntzrec  14169  dvdsr02  14521  01eq0ring  14605  rmodislmodlem  14796  rspsn  14980  zndvds  15093  znleval  15097  psrbagconf1o  15174  psr1clfi  15198  toponsspwpwg  15248  dmtopon  15249  hmeoimaf1o  15540  txhmeo  15545  limcmpted  15889  ioocosf1o  16082  fsumdvdsmul  16285  gausslemma2dlem0i  16381  lgseisenlem2  16395  lgsquadlem2  16402  2lgslem1c  16414  2lgsoddprmlem2  16430  2lgsoddprm  16437  uspgredgiedg  16624  uspgriedgedg  16625  uspgr2wlkeq  16811  wlk0prc  16818  wlklenvclwlk  16819  eupth2lem2dc  16905  bj-peano4  17186  pwle2  17233  subctctexmid  17235  pw1nct  17238  rabid1o  17239  stnot  17244  exmidsbthrlem  17273  iooref1o  17289  iswomni0  17308