MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqrdv Structured version   Unicode version

Theorem eqrdv 2379
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
Assertion
Ref Expression
eqrdv  |-  ( ph  ->  A  =  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
21alrimiv 1727 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2375 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 212 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1397    = wceq 1399    e. wcel 1826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374
This theorem is referenced by:  eqrdav  2380  eqrdavOLD  2381  uneq1  3565  ineq1  3607  unineq  3673  difin2  3685  difsn  4078  intmin4  4229  iunconst  4252  iinconst  4253  dfiun2g  4275  iindif2  4312  iinin2  4313  iunxsng  4325  opthprc  4961  inimasn  5333  dmsnopg  5387  dfco2a  5415  iotaeq  5468  imadif  5571  ssimaex  5839  unpreima  5915  respreima  5918  iinpreima  5919  fnsnb  5992  fmptsng  5994  fmptsnd  5995  tpres  6026  fconstfvOLD  6035  iunpw  6513  ordpwsuc  6549  ordsucun  6559  fun11iun  6659  reldm  6750  rntpos  6886  onoviun  6932  oarec  7129  iserd  7255  erth  7274  map0e  7375  ixpiin  7414  boxriin  7430  pw2f1olem  7540  fifo  7807  ordiso2  7855  finacn  8344  acnen  8347  acacni  8433  dfac13  8435  fin23lem26  8618  isf34lem4  8670  axdc3lem2  8744  fpwwe2lem8  8926  fpwwe2lem12  8930  fpwwe2lem13  8931  gch2  8964  gchac  8970  gchina  8988  genpass  9298  1idpr  9318  eqreznegel  11086  ixxun  11466  iccid  11495  difreicc  11573  iccsplit  11574  fzsplit2  11631  fzsn  11647  fzpr  11657  uzsplit  11672  fz1isolem  12414  pr2pwpr  12424  isercolllem2  13490  isercoll  13492  bitsmod  14088  bitscmp  14090  saddisj  14117  sadadd  14119  sadass  14123  smupvallem  14135  smueqlem  14142  smumul  14145  gcdcllem2  14152  vdwapun  14494  firest  14840  fncnvimaeqv  15506  mhmpropd  16089  subgacs  16353  eqgid  16370  ghmmhmb  16395  ghmpropd  16421  resscntz  16486  symg1bas  16538  lsmcom2  16792  lsmass  16805  ablnsg  16970  lsmcomx  16979  gsum2d2  17116  subgdmdprd  17194  dprd2d2  17206  unitpropd  17459  subsubrg2  17569  subrgpropd  17576  rhmpropd  17577  abvpropd  17604  lssacs  17726  lssats2  17759  lsspropd  17776  lmhmpropd  17832  lbspropd  17858  unitgOLD  19554  discld  19676  neiptopnei  19719  neiptopreu  19720  restsn  19757  restdis  19765  neitr  19767  restlp  19770  cndis  19878  cnindis  19879  cnpdis  19880  lpcls  19951  hausmapdom  20086  ptpjpre1  20157  tx1cn  20195  tx2cn  20196  hauseqlcld  20232  txkgen  20238  idqtop  20292  tgqtop  20298  acufl  20503  uffix  20507  ufildr  20517  fmfg  20535  rnelfm  20539  fmfnfm  20544  fmid  20546  fmco  20547  flimrest  20569  fclsrest  20610  alexsubALT  20636  tsmsgsum  20722  tsmsgsumOLD  20725  tsmssubm  20729  tsmsresOLD  20730  tsmsres  20731  tsmsf1o  20732  xpsdsval  20969  blpnf  20985  blin  21009  blres  21019  xmetec  21022  imasf1obl  21076  imasf1oxms  21077  prdsbl  21079  metrest  21112  metutopOLD  21170  psmetutop  21171  restmetu  21175  dscopn  21179  cnbl0  21366  bl2ioo  21382  xrtgioo  21396  cncfmet  21497  icoopnst  21524  iocopnst  21525  cldcss2  21942  iunmbl2  22052  mbfmulc2lem  22139  mbfmax  22141  ismbf3d  22146  mbfimaopnlem  22147  mbfaddlem  22152  mbfsup  22156  i1f1lem  22181  i1faddlem  22185  i1fmullem  22186  i1fmulclem  22194  i1fres  22197  mbfi1fseqlem4  22210  limcdif  22365  limcnlp  22367  limcflf  22370  limcres  22375  limcun  22384  ply1remlem  22648  fta1glem2  22652  plypf1  22694  ofmulrt  22763  plyremlem  22785  aannenlem1  22809  tglineelsb2  24132  tglinecom  24135  cusgrarn  24580  uvtxnbgra  24614  clwwlknscsh  24940  2wot2wont  25007  2spot2iun2spont  25012  nbhashuvtx  25037  vdiscusgra  25042  rusgranumwlkb0  25074  eupath2  25101  usg2spot2nb  25186  usgreg2spot  25188  numclwwlkun  25200  ubthlem1  25903  ocin  26331  shscom  26354  spansncol  26603  iunxsngf  27553  iunsnima  27604  unipreima  27624  1stpreimas  27671  1stpreima  27672  2ndpreima  27673  fpwrelmapffslem  27705  iocinioc2  27743  nndiffz1  27749  fzsplit3  27752  fimaproj  27990  qtophaus  27993  locfinreflem  27997  prsdm  28050  prsrn  28051  indpi1  28170  indf1ofs  28174  1stmbfm  28387  2ndmbfm  28388  mbfmcnt  28395  eulerpartlemgh  28500  dstfrvunirn  28596  preduz  29445  predfz  29448  ontgval  30049  heicant  30214  neifg  30355  filnetlem4  30365  istotbnd3  30433  sstotbnd  30437  ismtyima  30465  heibor  30483  divrngidl  30591  prtlem19  30785  prter2  30788  mzpmfp  30845  lzunuz  30866  fz1eqin  30867  jm2.23  31104  pw2f1ocnv  31145  dfacbasgrp  31225  subrgacs  31317  sdrgacs  31318  rfcnpre3  31575  rfcnpre4  31576  unima  31608  iccshift  31724  iocopn  31726  iooshift  31728  iccintsng  31729  icoopn  31731  limcdm0  31790  limcresiooub  31814  limcresioolb  31815  fperdvper  31881  itgperiod  31946  fourierdlem32  32087  fourierdlem33  32088  fourierdlem48  32103  fourierdlem49  32104  fourierdlem81  32136  mgmhmpropd  32791  rnghmval2  32901  csbabgOLD  33961  lkrsc  35235  lshpkr  35255  paddvaln0N  35938  paddval0  35947  diaglbN  37195  cdlemm10N  37258  lcfrvalsnN  37681  lcfrlem9  37690  lcdlss  37759  mapd1o  37788  mapd0  37805  hlhillcs  38101
  Copyright terms: Public domain W3C validator