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

Theorem eqrdv 2281
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 1617 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2277 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 203 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eqrdav  2282  csbcomg  3104  csbabg  3142  uneq1  3322  ineq1  3363  unineq  3419  difin2  3430  difsn  3755  intmin4  3891  iunconst  3913  iinconst  3914  dfiun2g  3935  iindif2  3971  iinin2  3972  iunxsng  3980  iunpw  4570  ordpwsuc  4606  ordsucun  4616  opthprc  4736  dmsnopg  5144  dfco2a  5173  iotaeq  5227  imadif  5327  fun11iun  5493  ssimaex  5584  unpreima  5651  respreima  5654  iinpreima  5655  fconstfv  5734  reldm  6171  rntpos  6247  onoviun  6360  oarec  6560  iserd  6686  erth  6704  map0e  6805  ixpiin  6842  boxriin  6858  pw2f1olem  6966  fifo  7185  ordiso2  7230  finacn  7677  acnen  7680  acacni  7766  dfac13  7768  fin23lem26  7951  isf34lem4  8003  axdc3lem2  8077  fpwwe2lem8  8259  fpwwe2lem12  8263  fpwwe2lem13  8264  gchac  8295  gch2  8301  gchina  8321  genpass  8633  1idpr  8653  eqreznegel  10303  ixxun  10672  iccid  10701  difreicc  10767  iccsplit  10768  fzsplit2  10815  fzsn  10833  fzpr  10840  uzsplit  10855  fz1isolem  11399  isercolllem2  12139  isercoll  12141  bitsmod  12627  bitscmp  12629  saddisj  12656  sadadd  12658  sadass  12662  smupvallem  12674  smueqlem  12681  smumul  12684  gcdcllem2  12691  vdwapun  13021  firest  13337  mhmpropd  14421  subgacs  14652  eqgid  14669  ghmmhmb  14694  ghmpropd  14720  resscntz  14807  lsmcom2  14966  lsmass  14979  ablnsg  15139  lsmcomx  15148  gsum2d2  15225  subgdmdprd  15269  dprd2d2  15279  unitpropd  15479  subsubrg2  15572  subrgpropd  15579  rhmpropd  15580  abvpropd  15607  lssacs  15724  lssats2  15757  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  unitg  16705  discld  16826  restsn  16901  restdis  16909  restlp  16913  cndis  17019  cnindis  17020  cnpdis  17021  lpcls  17092  hausmapdom  17226  ptpjpre1  17266  tx1cn  17303  tx2cn  17304  hauseqlcld  17340  txkgen  17346  idqtop  17397  tgqtop  17403  acufl  17612  uffix  17616  ufildr  17626  fmfg  17644  rnelfm  17648  fmfnfm  17653  fmid  17655  fmco  17656  flimrest  17678  fclsrest  17719  alexsubALT  17745  tsmsgsum  17821  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  xpsdsval  17945  blpnf  17954  blin  17970  blres  17977  xmetec  17980  imasf1obl  18034  imasf1oxms  18035  prdsbl  18037  metrest  18070  dscopn  18096  cnbl0  18283  bl2ioo  18298  xrtgioo  18312  cncfmet  18412  icoopnst  18437  iocopnst  18438  cldcss2  18806  iunmbl2  18914  mbfmulc2lem  19002  mbfmax  19004  ismbf3d  19009  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  i1f1lem  19044  i1faddlem  19048  i1fmullem  19049  i1fmulclem  19057  i1fres  19060  mbfi1fseqlem4  19073  limcdif  19226  limcnlp  19228  limcflf  19231  limcres  19236  limcun  19245  ply1remlem  19548  fta1glem2  19552  plypf1  19594  ofmulrt  19662  plyremlem  19684  aannenlem1  19708  ubthlem1  21449  ocin  21875  shscom  21898  spansncol  22147  fzsplit3  23031  unipreima  23209  iocinioc2  23272  1stmbfm  23565  2ndmbfm  23566  mbfmcnt  23573  indpi1  23605  indf1ofs  23609  dstfrvunirn  23675  eupath2  23904  preduz  24200  predfz  24203  ontgval  24870  splint  25048  iscst4  25177  prsubrtr  25399  fgsb2  25555  iint  25612  dmrngcmp  25751  pdiveql  26168  abhp2  26175  bhp2a  26176  neifg  26320  filnetlem4  26330  istotbnd3  26495  sstotbnd  26499  ismtyima  26527  heibor  26545  divrngidl  26653  prtlem19  26746  prter2  26749  mzpmfp  26825  lzunuz  26847  fz1eqin  26848  jm2.23  27089  pw2f1ocnv  27130  dfacbasgrp  27273  subrgacs  27508  sdrgacs  27509  rfcnpre3  27704  rfcnpre4  27705  uvtxnbgra  28165  lkrsc  29287  lshpkr  29307  paddvaln0N  29990  paddval0  29999  diaglbN  31245  cdlemm10N  31308  lcfrvalsnN  31731  lcfrlem9  31740  lcdlss  31809  mapd1o  31838  mapd0  31855  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator