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

Theorem rexbidva 2714
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 1629 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2712 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 1725   E.wrex 2698
This theorem is referenced by:  2rexbiia  2731  2rexbidva  2738  rexeqbidva  2911  onfr  4612  frinxp  4935  dfimafn  5767  funimass4  5769  fconstfv  5946  fliftel  6023  fliftf  6029  isomin  6049  f1oiso  6063  releldm2  6389  oaass  6796  qsinxp  6972  qliftel  6979  fimaxg  7346  ordunifi  7349  supisolem  7467  wemapwe  7646  cflim2  8135  cfsmolem  8142  alephsing  8148  brdom7disj  8401  brdom6disj  8402  alephreg  8449  nqereu  8798  1idpr  8898  map2psrpr  8977  axsup  9143  rereccl  9724  sup3  9957  infm3  9959  creur  9986  creui  9987  nndiv  10032  nnrecl  10211  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem5  10596  supxrbnd1  10892  supxrbnd2  10893  supxrbnd  10899  expnlbnd  11501  limsuplt  12265  clim2  12290  clim2c  12291  clim0c  12293  ello12  12302  elo12  12313  rlimresb  12351  climabs0  12371  sumeq2ii  12479  mertens  12655  alzdvds  12891  oddm1even  12901  divalglem4  12908  divalgb  12916  vdwlem6  13346  vdwlem11  13351  vdw  13354  ramval  13368  imasleval  13758  isipodrs  14579  ipodrsfi  14581  mndpropd  14713  grppropd  14815  conjnmzb  15032  sylow1lem2  15225  sylow3lem1  15253  sylow3lem3  15255  lsmelvalm  15277  lsmass  15294  iscyg3  15488  ghmcyg  15497  cycsubgcyg  15502  pgpfac1lem2  15625  pgpfac1lem4  15628  ablfac2  15639  dvdsr02  15753  crngunit  15759  dvdsrpropd  15793  lpigen  16319  znunit  16836  isclo  17143  iscnp3  17300  lmbrf  17316  cncnp  17336  lmss  17354  isnrm2  17414  cmpfi  17463  bwth  17465  1stcfb  17500  1stccnp  17517  ptrescn  17663  txkgen  17676  xkoinjcn  17711  trfil3  17912  fmid  17984  lmflf  18029  txflf  18030  ptcmplem3  18077  tsmsf1o  18166  ucnprima  18304  metrest  18546  metcnp  18563  metcnp2  18564  txmetcnp  18569  metuel2  18601  metustblOLD  18602  metustbl  18603  metutopOLD  18604  psmetutop  18605  metucnOLD  18610  metucn  18611  evth2  18977  lmmbrf  19207  iscfil2  19211  fmcfil  19217  iscau2  19222  iscau4  19224  iscauf  19225  caucfil  19228  iscmet3lem3  19235  cfilresi  19240  causs  19243  lmclim  19247  ivth2  19344  ovolfioo  19356  ovolficc  19357  ovolshftlem1  19397  ovolscalem1  19401  volsup2  19489  ismbf3d  19538  mbfaddlem  19544  mbfsup  19548  mbfinf  19549  itg2seq  19626  itg2gt0  19644  ellimc2  19756  ellimc3  19758  rolle  19866  cmvth  19867  mvth  19868  dvlip  19869  dvivth  19886  lhop1lem  19889  deg1ldg  20007  ulm2  20293  ulmdvlem3  20310  dcubic  20678  mcubic  20679  cubic2  20680  rlimcnp  20796  ftalem3  20849  isppw2  20890  lgsquadlem2  21131  dchrmusumlema  21179  dchrisum0lema  21200  nmobndi  22268  nmounbi  22269  nmoo0  22284  h2hcau  22474  h2hlm  22475  shsel3  22809  pjhtheu2  22910  chscllem2  23132  adjbdln  23578  branmfn  23600  pjimai  23671  chrelati  23859  cdj3lem3  23933  cdj3lem3b  23935  dfimafnf  24035  ofpreima  24073  gsumpropd2lem  24212  isarchi2  24247  lmdvg  24330  esumfsup  24452  dya2icoseg2  24620  ballotlemodife  24747  ballotlemsima  24765  erdszelem10  24878  iscvm  24938  prodeq2ii  25231  zprod  25255  wsuclem  25568  axsegcon  25858  axpasch  25872  axcontlem7  25901  seglelin  26042  outsideofeu  26057  supadd  26229  mblfinlem  26234  opnrebl  26314  opnrebl2  26315  filnetlem4  26401  lmclim2  26455  caures  26457  isbnd3b  26485  heiborlem7  26517  heiborlem10  26520  rrncmslem  26532  isdrngo2  26565  prter3  26722  elrfirn  26740  elrfirn2  26741  mrefg3  26753  diophin  26822  diophun  26823  diophren  26865  rmxycomplete  26971  wepwsolem  27107  fnwe2lem2  27117  islssfg  27136  elfilspd  27223  dfaimafn  27996  usgra2pth0  28265  el2spthonot0  28291  usg2spthonot1  28310  usgreg2spot  28393  islshpsm  29715  lsatfixedN  29744  lrelat  29749  eqlkr2  29835  lshpkrlem1  29845  lfl1dim  29856  eqlkr4  29900  ishlat3N  30089  hlsupr2  30121  hlrelat5N  30135  hlrelat  30136  cvrval5  30149  cvrat42  30178  athgt  30190  3dim0  30191  islln3  30244  llnexatN  30255  islpln3  30267  islvol3  30310  islvol5  30313  isline4N  30511  polval2N  30640  4atex3  30815  cdleme0ex2N  30958  cdlemefrs29cpre1  31132  cdlemb3  31340  cdlemg33c  31442  cdlemg33e  31444  dia1dim2  31797  cdlemm10N  31853  dib1dim2  31903  diclspsn  31929  dih1dimatlem  32064  dihatexv2  32074  djhcvat42  32150  dihjat1lem  32163  dvh4dimat  32173  dvh2dimatN  32175  lcfrlem9  32285  mapdval4N  32367  mapdcv  32395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator