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

Theorem eqrdv 2440
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 1706 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2436 . 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 1381    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  eqrdav  2441  eqrdavOLD  2442  uneq1  3636  ineq1  3678  unineq  3733  difin2  3745  csbcomgOLD  3824  csbabgOLD  3842  difsn  4149  intmin4  4301  iunconst  4324  iinconst  4325  dfiun2g  4347  iindif2  4384  iinin2  4385  iunxsng  4394  opthprc  5037  inimasn  5413  dmsnopg  5469  dfco2a  5497  iotaeq  5549  imadif  5653  ssimaex  5923  unpreima  5998  respreima  6001  iinpreima  6002  fnsnb  6075  fmptsng  6077  fmptsnd  6078  fconstfvOLD  6119  iunpw  6599  ordpwsuc  6635  ordsucun  6645  fun11iun  6745  reldm  6836  rntpos  6970  onoviun  7016  oarec  7213  iserd  7339  erth  7358  map0e  7458  ixpiin  7497  boxriin  7513  pw2f1olem  7623  fifo  7894  ordiso2  7943  finacn  8434  acnen  8437  acacni  8523  dfac13  8525  fin23lem26  8708  isf34lem4  8760  axdc3lem2  8834  fpwwe2lem8  9018  fpwwe2lem12  9022  fpwwe2lem13  9023  gch2  9056  gchac  9062  gchina  9080  genpass  9390  1idpr  9410  eqreznegel  11176  ixxun  11554  iccid  11583  difreicc  11661  iccsplit  11662  fzsplit2  11719  fzsn  11734  fzpr  11744  uzsplit  11759  fz1isolem  12489  pr2pwpr  12499  isercolllem2  13467  isercoll  13469  bitsmod  13963  bitscmp  13965  saddisj  13992  sadadd  13994  sadass  13998  smupvallem  14010  smueqlem  14017  smumul  14020  gcdcllem2  14027  vdwapun  14369  firest  14707  mhmpropd  15846  subgacs  16110  eqgid  16127  ghmmhmb  16152  ghmpropd  16178  resscntz  16243  symg1bas  16295  lsmcom2  16549  lsmass  16562  ablnsg  16727  lsmcomx  16736  gsum2d2  16876  subgdmdprd  16955  dprd2d2  16967  unitpropd  17220  subsubrg2  17330  subrgpropd  17337  rhmpropd  17338  abvpropd  17365  lssacs  17487  lssats2  17520  lsspropd  17537  lmhmpropd  17593  lbspropd  17619  unitgOLD  19342  discld  19463  neiptopnei  19506  neiptopreu  19507  restsn  19544  restdis  19552  neitr  19554  restlp  19557  cndis  19665  cnindis  19666  cnpdis  19667  lpcls  19738  hausmapdom  19874  ptpjpre1  19945  tx1cn  19983  tx2cn  19984  hauseqlcld  20020  txkgen  20026  idqtop  20080  tgqtop  20086  acufl  20291  uffix  20295  ufildr  20305  fmfg  20323  rnelfm  20327  fmfnfm  20332  fmid  20334  fmco  20335  flimrest  20357  fclsrest  20398  alexsubALT  20424  tsmsgsum  20510  tsmsgsumOLD  20513  tsmssubm  20517  tsmsresOLD  20518  tsmsres  20519  tsmsf1o  20520  xpsdsval  20757  blpnf  20773  blin  20797  blres  20807  xmetec  20810  imasf1obl  20864  imasf1oxms  20865  prdsbl  20867  metrest  20900  metutopOLD  20958  psmetutop  20959  restmetu  20963  dscopn  20967  cnbl0  21154  bl2ioo  21170  xrtgioo  21184  cncfmet  21285  icoopnst  21312  iocopnst  21313  cldcss2  21730  iunmbl2  21840  mbfmulc2lem  21927  mbfmax  21929  ismbf3d  21934  mbfimaopnlem  21935  mbfaddlem  21940  mbfsup  21944  i1f1lem  21969  i1faddlem  21973  i1fmullem  21974  i1fmulclem  21982  i1fres  21985  mbfi1fseqlem4  21998  limcdif  22153  limcnlp  22155  limcflf  22158  limcres  22163  limcun  22172  ply1remlem  22436  fta1glem2  22440  plypf1  22482  ofmulrt  22550  plyremlem  22572  aannenlem1  22596  tglineelsb2  23884  tglinecom  23887  cusgrarn  24331  uvtxnbgra  24365  clwwlknscsh  24691  2wot2wont  24758  2spot2iun2spont  24763  nbhashuvtx  24788  vdiscusgra  24793  rusgranumwlkb0  24825  eupath2  24852  usg2spot2nb  24937  usgreg2spot  24939  numclwwlkun  24951  ubthlem1  25658  ocin  26086  shscom  26109  spansncol  26358  unipreima  27356  1stpreima  27396  2ndpreima  27397  fpwrelmapffslem  27427  iocinioc2  27462  nndiffz1  27468  fzsplit3  27471  fimaproj  27709  qtophaus  27712  locfinreflem  27716  prsdm  27769  prsrn  27770  indpi1  27908  indf1ofs  27912  1stmbfm  28104  2ndmbfm  28105  mbfmcnt  28112  eulerpartlemgh  28190  dstfrvunirn  28286  preduz  29255  predfz  29258  ontgval  29871  heicant  30024  neifg  30164  filnetlem4  30174  istotbnd3  30242  sstotbnd  30246  ismtyima  30274  heibor  30292  divrngidl  30400  prtlem19  30594  prter2  30597  mzpmfp  30654  mzpmfpOLD  30655  lzunuz  30676  fz1eqin  30677  jm2.23  30913  pw2f1ocnv  30954  dfacbasgrp  31032  subrgacs  31125  sdrgacs  31126  rfcnpre3  31362  rfcnpre4  31363  unima  31391  iccshift  31494  iocopn  31496  iooshift  31498  iccintsng  31499  icoopn  31501  limcdm0  31532  limcresiooub  31556  limcresioolb  31557  fperdvper  31619  itgperiod  31670  fourierdlem32  31810  fourierdlem33  31811  fourierdlem48  31826  fourierdlem49  31827  fourierdlem81  31859  mgmhmpropd  32311  tpres  32390  rnghmval2  32419  fncnvimaeqv  32475  lkrsc  34562  lshpkr  34582  paddvaln0N  35265  paddval0  35274  diaglbN  36522  cdlemm10N  36585  lcfrvalsnN  37008  lcfrlem9  37017  lcdlss  37086  mapd1o  37115  mapd0  37132  hlhillcs  37428
  Copyright terms: Public domain W3C validator