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

Theorem eqrdv 2460
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 1784 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2456 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 217 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453    = wceq 1455    e. wcel 1898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  eqrdav  2461  uneq1  3593  ineq1  3639  unineq  3705  difin2  3717  difsn  4119  intmin4  4278  iunconst  4301  iinconst  4302  dfiun2g  4324  iindif2  4361  iinin2  4362  iunxsng  4374  opthprc  4901  inimasn  5272  dmsnopg  5326  dfco2a  5354  iotaeq  5573  imadif  5680  ssimaex  5953  unpreima  6029  respreima  6032  iinpreima  6033  fnsnb  6107  fmptsng  6109  fmptsnd  6110  tpres  6141  fconstfvOLD  6152  iunpw  6632  ordpwsuc  6669  ordsucun  6679  fun11iun  6780  reldm  6871  rntpos  7012  onoviun  7088  oarec  7289  iserd  7415  erth  7434  map0e  7535  ixpiin  7574  boxriin  7590  pw2f1olem  7702  fifo  7972  ordiso2  8056  finacn  8507  acnen  8510  acacni  8596  dfac13  8598  fin23lem26  8781  isf34lem4  8833  axdc3lem2  8907  fpwwe2lem8  9088  fpwwe2lem12  9092  fpwwe2lem13  9093  gch2  9126  gchac  9132  gchina  9150  genpass  9460  1idpr  9480  eqreznegel  11278  ixxun  11680  iccid  11710  difreicc  11793  iccsplit  11794  fzsplit2  11853  fzsn  11869  fzpr  11880  uzsplit  11895  preduz  11942  predfz  11945  fz1isolem  12657  pr2pwpr  12669  isercolllem2  13778  isercoll  13780  bitsmod  14459  bitscmp  14461  saddisj  14488  sadadd  14490  sadass  14494  smupvallem  14506  smueqlem  14513  smumul  14516  gcdcllem2  14523  vdwapun  14973  firest  15380  fncnvimaeqv  16054  mhmpropd  16637  subgacs  16901  eqgid  16918  ghmmhmb  16943  ghmpropd  16969  resscntz  17034  symg1bas  17086  lsmcom2  17356  lsmass  17369  ablnsg  17534  lsmcomx  17543  gsum2d2  17655  subgdmdprd  17716  dprd2d2  17726  unitpropd  17974  subsubrg2  18084  subrgpropd  18091  rhmpropd  18092  abvpropd  18119  lssacs  18239  lssats2  18272  lsspropd  18289  lmhmpropd  18345  lbspropd  18371  unitgOLD  20032  discld  20154  neiptopnei  20197  neiptopreu  20198  restsn  20235  restdis  20243  neitr  20245  restlp  20248  cndis  20356  cnindis  20357  cnpdis  20358  lpcls  20429  hausmapdom  20564  ptpjpre1  20635  tx1cn  20673  tx2cn  20674  hauseqlcld  20710  txkgen  20716  idqtop  20770  tgqtop  20776  acufl  20981  uffix  20985  ufildr  20995  fmfg  21013  rnelfm  21017  fmfnfm  21022  fmid  21024  fmco  21025  flimrest  21047  fclsrest  21088  alexsubALT  21115  tsmsgsum  21202  tsmssubm  21206  tsmsres  21207  tsmsf1o  21208  xpsdsval  21445  blpnf  21461  blin  21485  blres  21495  xmetec  21498  imasf1obl  21552  imasf1oxms  21553  prdsbl  21555  metrest  21588  psmetutop  21631  restmetu  21634  dscopn  21637  cnbl0  21843  bl2ioo  21859  xrtgioo  21873  cncfmet  21989  icoopnst  22016  iocopnst  22017  cldcss2  22445  iunmbl2  22559  mbfmulc2lem  22652  mbfmax  22654  ismbf3d  22659  mbfimaopnlem  22660  mbfaddlem  22665  mbfsup  22669  i1f1lem  22696  i1faddlem  22700  i1fmullem  22701  i1fmulclem  22709  i1fres  22712  mbfi1fseqlem4  22725  limcdif  22880  limcnlp  22882  limcflf  22885  limcres  22890  limcun  22899  ply1remlem  23162  fta1glem2  23166  plypf1  23215  ofmulrt  23284  plyremlem  23306  aannenlem1  23333  tglineelsb2  24726  tglinecom  24729  cusgrarn  25236  uvtxnbgra  25270  clwwlknscsh  25596  2wot2wont  25663  2spot2iun2spont  25668  nbhashuvtx  25693  vdiscusgra  25698  rusgranumwlkb0  25730  eupath2  25757  usg2spot2nb  25842  usgreg2spot  25844  numclwwlkun  25856  ubthlem1  26561  ocin  26998  shscom  27021  spansncol  27270  iunxsngf  28221  iunsnima  28273  unipreima  28294  1stpreimas  28335  1stpreima  28336  2ndpreima  28337  fpwrelmapffslem  28366  iocinioc2  28410  nndiffz1  28415  fzsplit3  28419  smatrcl  28671  fimaproj  28709  qtophaus  28712  locfinreflem  28716  prsdm  28769  prsrn  28770  indpi1  28892  indf1ofs  28896  1stmbfm  29131  2ndmbfm  29132  mbfmcnt  29139  eulerpartlemgh  29260  dstfrvunirn  29356  neifg  31076  filnetlem4  31086  ontgval  31140  mptsnunlem  31785  finxpsuclem  31834  poimirlem16  32001  poimirlem19  32004  poimirlem23  32008  poimirlem27  32012  heicant  32020  istotbnd3  32148  sstotbnd  32152  ismtyima  32180  heibor  32198  divrngidl  32306  prtlem19  32495  prter2  32498  lkrsc  32708  lshpkr  32728  paddvaln0N  33411  paddval0  33420  diaglbN  34668  cdlemm10N  34731  lcfrvalsnN  35154  lcfrlem9  35163  lcdlss  35232  mapd1o  35261  mapd0  35278  hlhillcs  35574  mzpmfp  35634  lzunuz  35655  fz1eqin  35656  jm2.23  35896  pw2f1ocnv  35937  dfacbasgrp  36012  subrgacs  36111  sdrgacs  36112  inintabd  36230  cnvcnvintabd  36251  cnvintabd  36254  csbabgOLD  37251  rfcnpre3  37394  rfcnpre4  37395  iunxsngf2  37440  unima  37467  iccshift  37657  iocopn  37659  iooshift  37661  iccintsng  37662  icoopn  37664  limcdm0  37736  limcresiooub  37761  limcresioolb  37762  fperdvper  37828  itgperiod  37896  fourierdlem32  38040  fourierdlem33  38041  fourierdlem48  38056  fourierdlem49  38057  fourierdlem81  38089  iccpartiun  38786  ushgredgedga  39356  ushgredgedgaloop  39358  nbumgrvtx  39464  nbusgrvtxm1uvtx  39528  vdiscusgr  39618  mgmhmpropd  40058  rnghmval2  40168
  Copyright terms: Public domain W3C validator