Theorem eqcom 2195

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 2187	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2187	. 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 2164

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 2175

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

This theorem is referenced by:  eqcoms  2196  eqcomi  2197  neqcomd  2198  eqcomd  2199  eqeq2  2203  eqtr2  2212  eqtr3  2213  abeq1  2303  nesym  2409  pm13.181  2446  necom  2448  gencbvex  2807  gencbval  2809  clel5  2898  eqsbc2  3047  dfss  3168  dfss5  3365  rabrsndc  3687  preqr1g  3793  preqr1  3795  invdisj  4024  opthg2  4269  copsex4g  4277  opcom  4280  opeqsn  4282  opeqpr  4283  reusv3  4492  suc11g  4590  opthprc  4711  elxp3  4714  relop  4813  dmopab3  4876  rncoeq  4936  restidsing  4999  dfrel4v  5118  dmsnm  5132  iota1  5230  sniota  5246  dffn5im  5603  fvelrnb  5605  dfimafn2  5607  funimass4  5608  fnsnfv  5617  dmfco  5626  fndmdif  5664  fneqeql  5667  rexrn  5696  ralrn  5697  elrnrexdmb  5699  dffo4  5707  ftpg  5743  fconstfvm  5777  foima2  5795  rexima  5798  ralima  5799  dff13  5812  f1eqcocnv  5835  eusvobj2  5905  f1ocnvfv3  5908  oprabid  5951  eloprabga  6006  ovelimab  6071  dfoprab3  6246  f1o2ndf1  6283  cnvoprab  6289  brtpos2  6306  tpossym  6331  frecsuclem  6461  nntri3or  6548  erth2  6636  brecop  6681  erovlem  6683  ecopovsym  6687  ecopovsymg  6690  xpcomco  6882  mapen  6904  nneneq  6915  supelti  7063  djuf1olem  7114  eldju  7129  omp1eomlem  7155  nninfwlporlemd  7233  exmidontriimlem3  7285  ordpipqqs  7436  addcanprg  7678  ltsrprg  7809  caucvgsrlemcl  7851  caucvgsrlemfv  7853  elreal  7890  ltresr  7901  axcaucvglemcl  7957  axcaucvglemval  7959  addsubeq4  8236  subcan2  8246  negcon1  8273  negcon2  8274  addid0  8394  divmulap2  8697  conjmulap  8750  rerecclap  8751  creur  8980  creui  8981  nndiv  9025  elznn0  9335  zltnle  9366  uzm1  9626  divfnzn  9689  zq  9694  icoshftf1o  10060  iccf1o  10073  fzen  10112  fzneuz  10170  4fvwrd4  10209  qltnle  10316  flqeqceilz  10392  modq0  10403  modqmuladdnn0  10442  addmodlteq  10472  nn0ennn  10507  uzennn  10510  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  seq3f1olemstep  10588  exp3val  10615  qsqeqor  10724  hashfacen  10910  cjreb  11013  caucvgrelemrec  11126  minmax  11376  xrnegiso  11408  xrnegcon1d  11410  xrminmax  11411  pwm1geoserap1  11654  dvdsval2  11936  dvdsabseq  11992  dvdsflip  11996  odd2np1  12017  oddm1even  12019  sqoddm1div8z  12030  m1exp1  12045  divalgb  12069  modremain  12073  zeqzmulgcd  12110  dfgcd2  12154  divgcdcoprm0  12242  prm2orodd  12267  hashdvds  12362  oddprmdvds  12495  oddennn  12552  evenennn  12553  gsumval2  12983  grpid  13114  grpinvcnv  13143  grplmulf1o  13149  grpsubeq0  13161  grpsubadd  13163  grplactcnv  13177  isnsg4  13285  eqg0el  13302  conjghm  13349  conjnmzb  13353  dvdsr02  13604  01eq0ring  13688  rmodislmodlem  13849  rspsn  14033  zndvds  14148  znleval  14152  toponsspwpwg  14201  dmtopon  14202  hmeoimaf1o  14493  txhmeo  14498  limcmpted  14842  ioocosf1o  15030  gausslemma2dlem0i  15214  lgseisenlem2  15228  lgsquadlem2  15235  2lgslem1c  15247  2lgsoddprmlem2  15263  2lgsoddprm  15270  bj-peano4  15517  pwle2  15559  subctctexmid  15561  pw1nct  15563  exmidsbthrlem  15582  iooref1o  15594  iswomni0  15611