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

Theorem rexbidva 2668
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rexbidva  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rexbidva
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2666 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1717   E.wrex 2652
This theorem is referenced by:  2rexbiia  2685  2rexbidva  2692  rexeqbidva  2864  onfr  4563  frinxp  4885  dfimafn  5716  funimass4  5718  fconstfv  5895  fliftel  5972  fliftf  5978  isomin  5998  f1oiso  6012  releldm2  6338  oaass  6742  qsinxp  6918  qliftel  6925  fimaxg  7292  ordunifi  7295  supisolem  7410  wemapwe  7589  cflim2  8078  cfsmolem  8085  alephsing  8091  brdom7disj  8344  brdom6disj  8345  alephreg  8392  nqereu  8741  1idpr  8841  map2psrpr  8920  axsup  9086  rereccl  9666  sup3  9899  infm3  9901  creur  9928  creui  9929  nndiv  9974  nnrecl  10153  rpnnen1lem1  10534  rpnnen1lem2  10535  rpnnen1lem3  10536  rpnnen1lem5  10538  supxrbnd1  10834  supxrbnd2  10835  supxrbnd  10841  expnlbnd  11438  limsuplt  12202  clim2  12227  clim2c  12228  clim0c  12230  ello12  12239  elo12  12250  rlimresb  12288  climabs0  12308  sumeq2ii  12416  mertens  12592  alzdvds  12828  oddm1even  12838  divalglem4  12845  divalgb  12853  vdwlem6  13283  vdwlem11  13288  vdw  13291  ramval  13305  imasleval  13695  isipodrs  14516  ipodrsfi  14518  mndpropd  14650  grppropd  14752  conjnmzb  14969  sylow1lem2  15162  sylow3lem1  15190  sylow3lem3  15192  lsmelvalm  15214  lsmass  15231  iscyg3  15425  ghmcyg  15434  cycsubgcyg  15439  pgpfac1lem2  15562  pgpfac1lem4  15565  ablfac2  15576  dvdsr02  15690  crngunit  15696  dvdsrpropd  15730  lpigen  16256  znunit  16769  isclo  17076  iscnp3  17232  lmbrf  17248  cncnp  17268  lmss  17286  isnrm2  17346  cmpfi  17395  1stcfb  17431  1stccnp  17448  ptrescn  17594  txkgen  17607  xkoinjcn  17642  trfil3  17843  fmid  17915  lmflf  17960  txflf  17961  ptcmplem3  18008  tsmsf1o  18097  ucnprima  18235  metrest  18446  metcnp  18463  metcnp2  18464  txmetcnp  18469  metuel2  18487  metustbl  18488  metutop  18489  metucn  18492  evth2  18858  lmmbrf  19088  iscfil2  19092  fmcfil  19098  iscau2  19103  iscau4  19105  iscauf  19106  caucfil  19109  iscmet3lem3  19116  cfilresi  19121  causs  19124  lmclim  19128  ivth2  19221  ovolfioo  19233  ovolficc  19234  ovolshftlem1  19274  ovolscalem1  19278  volsup2  19366  ismbf3d  19415  mbfaddlem  19421  mbfsup  19425  mbfinf  19426  itg2seq  19503  itg2gt0  19521  ellimc2  19633  ellimc3  19635  rolle  19743  cmvth  19744  mvth  19745  dvlip  19746  dvivth  19763  lhop1lem  19766  deg1ldg  19884  ulm2  20170  ulmdvlem3  20187  dcubic  20555  mcubic  20556  cubic2  20557  rlimcnp  20673  ftalem3  20726  isppw2  20767  lgsquadlem2  21008  dchrmusumlema  21056  dchrisum0lema  21077  nmobndi  22126  nmounbi  22127  nmoo0  22142  h2hcau  22332  h2hlm  22333  shsel3  22667  pjhtheu2  22768  chscllem2  22990  adjbdln  23436  branmfn  23458  pjimai  23529  chrelati  23717  cdj3lem3  23791  cdj3lem3b  23793  dfimafnf  23888  gsumpropd2lem  24051  lmdvg  24144  esumfsup  24258  dya2icoseg2  24424  ballotlemodife  24536  ballotlemsima  24554  erdszelem10  24667  iscvm  24727  prodeq2ii  25020  zprod  25044  elfuns  25480  axsegcon  25582  axpasch  25596  axcontlem7  25625  seglelin  25766  outsideofeu  25781  supadd  25950  opnrebl  26016  opnrebl2  26017  filnetlem4  26103  lmclim2  26157  caures  26159  isbnd3b  26187  heiborlem7  26219  heiborlem10  26222  rrncmslem  26234  isdrngo2  26267  prter3  26424  elrfirn  26442  elrfirn2  26443  mrefg3  26455  diophin  26524  diophun  26525  diophren  26567  rmxycomplete  26673  wepwsolem  26809  fnwe2lem2  26819  islssfg  26839  elfilspd  26926  dfaimafn  27700  islshpsm  29097  lsatfixedN  29126  lrelat  29131  eqlkr2  29217  lshpkrlem1  29227  lfl1dim  29238  eqlkr4  29282  ishlat3N  29471  hlsupr2  29503  hlrelat5N  29517  hlrelat  29518  cvrval5  29531  cvrat42  29560  athgt  29572  3dim0  29573  islln3  29626  llnexatN  29637  islpln3  29649  islvol3  29692  islvol5  29695  isline4N  29893  polval2N  30022  4atex3  30197  cdleme0ex2N  30340  cdlemefrs29cpre1  30514  cdlemb3  30722  cdlemg33c  30824  cdlemg33e  30826  dia1dim2  31179  cdlemm10N  31235  dib1dim2  31285  diclspsn  31311  dih1dimatlem  31446  dihatexv2  31456  djhcvat42  31532  dihjat1lem  31545  dvh4dimat  31555  dvh2dimatN  31557  lcfrlem9  31667  mapdval4N  31749  mapdcv  31777
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-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-rex 2657
  Copyright terms: Public domain W3C validator