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

Theorem rexbidva 2666
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 2664 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 2650
This theorem is referenced by:  2rexbiia  2683  2rexbidva  2690  rexeqbidva  2862  onfr  4561  frinxp  4883  dfimafn  5714  funimass4  5716  fconstfv  5893  fliftel  5970  fliftf  5976  isomin  5996  f1oiso  6010  releldm2  6336  oaass  6740  qsinxp  6916  qliftel  6923  fimaxg  7290  ordunifi  7293  supisolem  7408  wemapwe  7587  cflim2  8076  cfsmolem  8083  alephsing  8089  brdom7disj  8342  brdom6disj  8343  alephreg  8390  nqereu  8739  1idpr  8839  map2psrpr  8918  axsup  9084  rereccl  9664  sup3  9897  infm3  9899  creur  9926  creui  9927  nndiv  9972  nnrecl  10151  rpnnen1lem1  10532  rpnnen1lem2  10533  rpnnen1lem3  10534  rpnnen1lem5  10536  supxrbnd1  10832  supxrbnd2  10833  supxrbnd  10839  expnlbnd  11436  limsuplt  12200  clim2  12225  clim2c  12226  clim0c  12228  ello12  12237  elo12  12248  rlimresb  12286  climabs0  12306  sumeq2ii  12414  mertens  12590  alzdvds  12826  oddm1even  12836  divalglem4  12843  divalgb  12851  vdwlem6  13281  vdwlem11  13286  vdw  13289  ramval  13303  imasleval  13693  isipodrs  14514  ipodrsfi  14516  mndpropd  14648  grppropd  14750  conjnmzb  14967  sylow1lem2  15160  sylow3lem1  15188  sylow3lem3  15190  lsmelvalm  15212  lsmass  15229  iscyg3  15423  ghmcyg  15432  cycsubgcyg  15437  pgpfac1lem2  15560  pgpfac1lem4  15563  ablfac2  15574  dvdsr02  15688  crngunit  15694  dvdsrpropd  15728  lpigen  16254  znunit  16767  isclo  17074  iscnp3  17230  lmbrf  17246  cncnp  17266  lmss  17284  isnrm2  17344  cmpfi  17393  1stcfb  17429  1stccnp  17446  ptrescn  17592  txkgen  17605  xkoinjcn  17640  trfil3  17841  fmid  17913  lmflf  17958  txflf  17959  ptcmplem3  18006  tsmsf1o  18095  ucnprima  18233  metrest  18444  metcnp  18461  metcnp2  18462  txmetcnp  18467  metuel2  18485  metustbl  18486  metutop  18487  metucn  18490  evth2  18856  lmmbrf  19086  iscfil2  19090  fmcfil  19096  iscau2  19101  iscau4  19103  iscauf  19104  caucfil  19107  iscmet3lem3  19114  cfilresi  19119  causs  19122  lmclim  19126  ivth2  19219  ovolfioo  19231  ovolficc  19232  ovolshftlem1  19272  ovolscalem1  19276  volsup2  19364  ismbf3d  19413  mbfaddlem  19419  mbfsup  19423  mbfinf  19424  itg2seq  19501  itg2gt0  19519  ellimc2  19631  ellimc3  19633  rolle  19741  cmvth  19742  mvth  19743  dvlip  19744  dvivth  19761  lhop1lem  19764  deg1ldg  19882  ulm2  20168  ulmdvlem3  20185  dcubic  20553  mcubic  20554  cubic2  20555  rlimcnp  20671  ftalem3  20724  isppw2  20765  lgsquadlem2  21006  dchrmusumlema  21054  dchrisum0lema  21075  nmobndi  22124  nmounbi  22125  nmoo0  22140  h2hcau  22330  h2hlm  22331  shsel3  22665  pjhtheu2  22766  chscllem2  22988  adjbdln  23434  branmfn  23456  pjimai  23527  chrelati  23715  cdj3lem3  23789  cdj3lem3b  23791  dfimafnf  23886  gsumpropd2lem  24049  lmdvg  24142  esumfsup  24256  dya2icoseg2  24422  ballotlemodife  24534  ballotlemsima  24552  erdszelem10  24665  iscvm  24725  prodeq2ii  25018  zprod  25042  elfuns  25478  axsegcon  25580  axpasch  25594  axcontlem7  25623  seglelin  25764  outsideofeu  25779  supadd  25948  opnrebl  26014  opnrebl2  26015  filnetlem4  26101  lmclim2  26155  caures  26157  isbnd3b  26185  heiborlem7  26217  heiborlem10  26220  rrncmslem  26232  isdrngo2  26265  prter3  26422  elrfirn  26440  elrfirn2  26441  mrefg3  26453  diophin  26522  diophun  26523  diophren  26565  rmxycomplete  26671  wepwsolem  26807  fnwe2lem2  26817  islssfg  26837  elfilspd  26924  dfaimafn  27698  islshpsm  29095  lsatfixedN  29124  lrelat  29129  eqlkr2  29215  lshpkrlem1  29225  lfl1dim  29236  eqlkr4  29280  ishlat3N  29469  hlsupr2  29501  hlrelat5N  29515  hlrelat  29516  cvrval5  29529  cvrat42  29558  athgt  29570  3dim0  29571  islln3  29624  llnexatN  29635  islpln3  29647  islvol3  29690  islvol5  29693  isline4N  29891  polval2N  30020  4atex3  30195  cdleme0ex2N  30338  cdlemefrs29cpre1  30512  cdlemb3  30720  cdlemg33c  30822  cdlemg33e  30824  dia1dim2  31177  cdlemm10N  31233  dib1dim2  31283  diclspsn  31309  dih1dimatlem  31444  dihatexv2  31454  djhcvat42  31530  dihjat1lem  31543  dvh4dimat  31553  dvh2dimatN  31555  lcfrlem9  31665  mapdval4N  31747  mapdcv  31775
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 2655
  Copyright terms: Public domain W3C validator