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

Theorem eqrdv 2402
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 1638 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2398 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 204 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eqrdav  2403  csbcomg  3234  csbabg  3270  uneq1  3454  ineq1  3495  unineq  3551  difin2  3563  difsn  3893  intmin4  4039  iunconst  4061  iinconst  4062  dfiun2g  4083  iindif2  4120  iinin2  4121  iunxsng  4129  iunpw  4718  ordpwsuc  4754  ordsucun  4764  opthprc  4884  inimasn  5248  dmsnopg  5300  dfco2a  5329  iotaeq  5385  imadif  5487  fun11iun  5654  ssimaex  5747  unpreima  5815  respreima  5818  iinpreima  5819  fconstfv  5913  reldm  6357  rntpos  6451  onoviun  6564  oarec  6764  iserd  6890  erth  6908  map0e  7010  ixpiin  7047  boxriin  7063  pw2f1olem  7171  fifo  7395  ordiso2  7440  finacn  7887  acnen  7890  acacni  7976  dfac13  7978  fin23lem26  8161  isf34lem4  8213  axdc3lem2  8287  fpwwe2lem8  8468  fpwwe2lem12  8472  fpwwe2lem13  8473  gchac  8504  gch2  8510  gchina  8530  genpass  8842  1idpr  8862  eqreznegel  10517  ixxun  10888  iccid  10917  difreicc  10984  iccsplit  10985  fzsplit2  11032  fzsn  11050  fzpr  11057  uzsplit  11073  fz1isolem  11665  isercolllem2  12414  isercoll  12416  bitsmod  12903  bitscmp  12905  saddisj  12932  sadadd  12934  sadass  12938  smupvallem  12950  smueqlem  12957  smumul  12960  gcdcllem2  12967  vdwapun  13297  firest  13615  mhmpropd  14699  subgacs  14930  eqgid  14947  ghmmhmb  14972  ghmpropd  14998  resscntz  15085  lsmcom2  15244  lsmass  15257  ablnsg  15417  lsmcomx  15426  gsum2d2  15503  subgdmdprd  15547  dprd2d2  15557  unitpropd  15757  subsubrg2  15850  subrgpropd  15857  rhmpropd  15858  abvpropd  15885  lssacs  15998  lssats2  16031  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  unitg  16987  discld  17108  neiptopnei  17151  neiptopreu  17152  restsn  17188  restdis  17196  neitr  17198  restlp  17201  cndis  17309  cnindis  17310  cnpdis  17311  lpcls  17382  hausmapdom  17516  ptpjpre1  17556  tx1cn  17594  tx2cn  17595  hauseqlcld  17631  txkgen  17637  idqtop  17691  tgqtop  17697  acufl  17902  uffix  17906  ufildr  17916  fmfg  17934  rnelfm  17938  fmfnfm  17943  fmid  17945  fmco  17946  flimrest  17968  fclsrest  18009  alexsubALT  18035  tsmsgsum  18121  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  xpsdsval  18364  blpnf  18380  blin  18404  blres  18414  xmetec  18417  imasf1obl  18471  imasf1oxms  18472  prdsbl  18474  metrest  18507  metutopOLD  18565  psmetutop  18566  restmetu  18570  dscopn  18574  cnbl0  18761  bl2ioo  18776  xrtgioo  18790  cncfmet  18891  icoopnst  18917  iocopnst  18918  cldcss2  19296  iunmbl2  19404  mbfmulc2lem  19492  mbfmax  19494  ismbf3d  19499  mbfimaopnlem  19500  mbfaddlem  19505  mbfsup  19509  i1f1lem  19534  i1faddlem  19538  i1fmullem  19539  i1fmulclem  19547  i1fres  19550  mbfi1fseqlem4  19563  limcdif  19716  limcnlp  19718  limcflf  19721  limcres  19726  limcun  19735  ply1remlem  20038  fta1glem2  20042  plypf1  20084  ofmulrt  20152  plyremlem  20174  aannenlem1  20198  cusgrarn  21421  uvtxnbgra  21455  eupath2  21655  ubthlem1  22325  ocin  22751  shscom  22774  spansncol  23023  unipreima  24009  1stpreima  24048  2ndpreima  24049  iocinioc2  24095  fzsplit3  24103  indpi1  24372  indf1ofs  24376  1stmbfm  24563  2ndmbfm  24564  mbfmcnt  24571  dstfrvunirn  24685  preduz  25414  predfz  25417  ontgval  26085  neifg  26290  filnetlem4  26300  istotbnd3  26370  sstotbnd  26374  ismtyima  26402  heibor  26420  divrngidl  26528  prtlem19  26617  prter2  26620  mzpmfp  26694  lzunuz  26716  fz1eqin  26717  jm2.23  26957  pw2f1ocnv  26998  dfacbasgrp  27141  subrgacs  27376  sdrgacs  27377  rfcnpre3  27571  rfcnpre4  27572  2wot2wont  28083  2spot2iun2spont  28088  usg2spot2nb  28168  usgreg2spot  28170  lkrsc  29580  lshpkr  29600  paddvaln0N  30283  paddval0  30292  diaglbN  31538  cdlemm10N  31601  lcfrvalsnN  32024  lcfrlem9  32033  lcdlss  32102  mapd1o  32131  mapd0  32148  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397
  Copyright terms: Public domain W3C validator