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  4379  copsex4g  4387  opcom  4391  opeqsn  4393  opeqpr  4394  reusv3  4606  suc11g  4704  opthprc  4826  elxp3  4829  relop  4930  dmopab3  4994  rncoeq  5056  restidsing  5119  dfrel4v  5239  dmsnm  5253  iota1  5352  sniota  5368  dffn5im  5748  fvelrnb  5750  dfimafn2  5752  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fneqeql  5817  rexrn  5845  ralrn  5846  elrnrexdmb  5848  dffo4  5856  ftpg  5899  fconstfvm  5933  dfimafnf  5955  foima2  5957  rexima  5960  ralima  5961  dff13  5974  f1eqcocnv  5997  riotaeqimp  6063  eusvobj2  6071  f1ocnvfv3  6074  oprabid  6117  eloprabga  6175  ovelimab  6240  dfoprab3  6425  f1o2ndf1  6464  cnvoprab  6470  brtpos2  6522  tpossym  6547  frecsuclem  6677  nntri3or  6766  erth2  6854  brecop  6899  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  xpcomco  7124  mapen  7146  nneneq  7158  supelti  7342  djuf1olem  7393  eldju  7408  omp1eomlem  7434  nninfwlporlemd  7512  exmidontriimlem3  7579  ordpipqqs  7741  addcanprg  7983  ltsrprg  8114  caucvgsrlemcl  8156  caucvgsrlemfv  8158  elreal  8195  ltresr  8206  axcaucvglemcl  8262  axcaucvglemval  8264  addsubeq4  8542  subcan2  8552  negcon1  8579  negcon2  8580  addid0  8700  addeq0  8704  divmulap2  9008  conjmulap  9061  rerecclap  9062  creur  9291  creui  9292  nndiv  9347  elznn0  9663  zltnle  9694  uzm1  9962  divfnzn  10030  zq  10035  icoshftf1o  10403  iccf1o  10417  fzen  10457  fzneuz  10518  4fvwrd4  10557  qltnle  10688  flqeqceilz  10768  modq0  10779  modqmuladdnn0  10818  addmodlteq  10848  nn0ennn  10883  uzennn  10886  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  seq3f1olemstep  10964  exp3val  10991  qsqeqor  11100  hashfacen  11298  hashf1lem1  11299  wrd2ind  11509  cjreb  11645  caucvgrelemrec  11759  minmax  12011  xrnegiso  12044  xrnegcon1d  12046  xrminmax  12047  pwm1geoserap1  12291  dvdsval2  12573  dvdsabseq  12630  dvdsflip  12634  odd2np1  12656  oddm1even  12658  sqoddm1div8z  12669  m1exp1  12684  divalgb  12708  modremain  12712  zeqzmulgcd  12763  dfgcd2  12807  divgcdcoprm0  12895  prm2orodd  12920  hashdvds  13019  oddprmdvds  13153  ballotfilemsima  13308  oddennn  13332  evenennn  13333  gzsumval2  13763  grpid  13893  grpinvcnv  13922  grplmulf1o  13928  grpsubeq0  13940  grpsubadd  13942  grplactcnv  13956  isnsg4  14064  eqg0el  14081  conjghm  14128  conjnmzb  14132  dvdsr02  14461  01eq0ring  14545  rmodislmodlem  14736  rspsn  14920  zndvds  15033  znleval  15037  psrbagconf1o  15113  psr1clfi  15128  toponsspwpwg  15172  dmtopon  15173  hmeoimaf1o  15464  txhmeo  15469  limcmpted  15813  ioocosf1o  16005  fsumdvdsmul  16186  gausslemma2dlem0i  16274  lgseisenlem2  16288  lgsquadlem2  16295  2lgslem1c  16307  2lgsoddprmlem2  16323  2lgsoddprm  16330  uspgredgiedg  16517  uspgriedgedg  16518  uspgr2wlkeq  16704  wlk0prc  16711  wlklenvclwlk  16712  eupth2lem2dc  16798  bj-peano4  17079  pwle2  17126  subctctexmid  17128  pw1nct  17131  rabid1o  17132  stnot  17137  exmidsbthrlem  17165  iooref1o  17181  iswomni0  17199