Theorem eqcom 2198

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 1484	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2190	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2190	. 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 2167

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqcoms  2199  eqcomi  2200  neqcomd  2201  eqcomd  2202  eqeq2  2206  eqtr2  2215  eqtr3  2216  abeq1  2306  nesym  2412  pm13.181  2449  necom  2451  gencbvex  2810  gencbval  2812  clel5  2901  eqsbc2  3050  dfss  3171  dfss5  3369  rabrsndc  3691  preqr1g  3797  preqr1  3799  invdisj  4028  opthg2  4273  copsex4g  4281  opcom  4284  opeqsn  4286  opeqpr  4287  reusv3  4496  suc11g  4594  opthprc  4715  elxp3  4718  relop  4817  dmopab3  4880  rncoeq  4940  restidsing  5003  dfrel4v  5122  dmsnm  5136  iota1  5234  sniota  5250  dffn5im  5609  fvelrnb  5611  dfimafn2  5613  funimass4  5614  fnsnfv  5623  dmfco  5632  fndmdif  5670  fneqeql  5673  rexrn  5702  ralrn  5703  elrnrexdmb  5705  dffo4  5713  ftpg  5749  fconstfvm  5783  foima2  5801  rexima  5804  ralima  5805  dff13  5818  f1eqcocnv  5841  eusvobj2  5911  f1ocnvfv3  5914  oprabid  5957  eloprabga  6013  ovelimab  6078  dfoprab3  6258  f1o2ndf1  6295  cnvoprab  6301  brtpos2  6318  tpossym  6343  frecsuclem  6473  nntri3or  6560  erth2  6648  brecop  6693  erovlem  6695  ecopovsym  6699  ecopovsymg  6702  xpcomco  6894  mapen  6916  nneneq  6927  supelti  7077  djuf1olem  7128  eldju  7143  omp1eomlem  7169  nninfwlporlemd  7247  exmidontriimlem3  7306  ordpipqqs  7458  addcanprg  7700  ltsrprg  7831  caucvgsrlemcl  7873  caucvgsrlemfv  7875  elreal  7912  ltresr  7923  axcaucvglemcl  7979  axcaucvglemval  7981  addsubeq4  8258  subcan2  8268  negcon1  8295  negcon2  8296  addid0  8416  divmulap2  8720  conjmulap  8773  rerecclap  8774  creur  9003  creui  9004  nndiv  9048  elznn0  9358  zltnle  9389  uzm1  9649  divfnzn  9712  zq  9717  icoshftf1o  10083  iccf1o  10096  fzen  10135  fzneuz  10193  4fvwrd4  10232  qltnle  10350  flqeqceilz  10427  modq0  10438  modqmuladdnn0  10477  addmodlteq  10507  nn0ennn  10542  uzennn  10545  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  seq3f1olemstep  10623  exp3val  10650  qsqeqor  10759  hashfacen  10945  cjreb  11048  caucvgrelemrec  11161  minmax  11412  xrnegiso  11444  xrnegcon1d  11446  xrminmax  11447  pwm1geoserap1  11690  dvdsval2  11972  dvdsabseq  12029  dvdsflip  12033  odd2np1  12055  oddm1even  12057  sqoddm1div8z  12068  m1exp1  12083  divalgb  12107  modremain  12111  zeqzmulgcd  12162  dfgcd2  12206  divgcdcoprm0  12294  prm2orodd  12319  hashdvds  12414  oddprmdvds  12548  oddennn  12634  evenennn  12635  gsumval2  13099  grpid  13241  grpinvcnv  13270  grplmulf1o  13276  grpsubeq0  13288  grpsubadd  13290  grplactcnv  13304  isnsg4  13418  eqg0el  13435  conjghm  13482  conjnmzb  13486  dvdsr02  13737  01eq0ring  13821  rmodislmodlem  13982  rspsn  14166  zndvds  14281  znleval  14285  psr1clfi  14316  toponsspwpwg  14342  dmtopon  14343  hmeoimaf1o  14634  txhmeo  14639  limcmpted  14983  ioocosf1o  15174  fsumdvdsmul  15311  gausslemma2dlem0i  15382  lgseisenlem2  15396  lgsquadlem2  15403  2lgslem1c  15415  2lgsoddprmlem2  15431  2lgsoddprm  15438  bj-peano4  15685  pwle2  15729  subctctexmid  15731  pw1nct  15734  exmidsbthrlem  15753  iooref1o  15765  iswomni0  15782