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

Theorem rexbidva 2562
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 1607 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2560 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1686   E.wrex 2546
This theorem is referenced by:  2rexbiia  2579  2rexbidva  2586  rexeqbidva  2753  onfr  4433  frinxp  4757  dfimafn  5573  funimass4  5575  fconstfv  5736  fliftel  5810  fliftf  5816  isomin  5836  f1oiso  5850  releldm2  6172  oaass  6561  qsinxp  6737  qliftel  6743  fimaxg  7106  ordunifi  7109  supisolem  7223  wemapwe  7402  cflim2  7891  cfsmolem  7898  alephsing  7904  brdom7disj  8158  brdom6disj  8159  alephreg  8206  nqereu  8555  1idpr  8655  map2psrpr  8734  axsup  8900  rereccl  9480  sup3  9713  infm3  9715  creur  9742  creui  9743  nndiv  9788  nnrecl  9965  rpnnen1lem1  10344  rpnnen1lem2  10345  rpnnen1lem3  10346  rpnnen1lem5  10348  supxrbnd1  10642  supxrbnd2  10643  supxrbnd  10649  expnlbnd  11233  limsuplt  11955  clim2  11980  clim2c  11981  clim0c  11983  ello12  11992  elo12  12003  rlimresb  12041  climabs0  12061  sumeq2ii  12168  mertens  12344  alzdvds  12580  oddm1even  12590  divalglem4  12597  divalgb  12605  vdwlem6  13035  vdwlem11  13040  vdw  13043  ramval  13057  imasleval  13445  isipodrs  14266  ipodrsfi  14268  mndpropd  14400  grppropd  14502  conjnmzb  14719  sylow1lem2  14912  sylow3lem1  14940  sylow3lem3  14942  lsmelvalm  14964  lsmass  14981  iscyg3  15175  ghmcyg  15184  cycsubgcyg  15189  pgpfac1lem2  15312  pgpfac1lem4  15315  ablfac2  15326  dvdsr02  15440  crngunit  15446  dvdsrpropd  15480  lpigen  16010  znunit  16519  isclo  16826  iscnp3  16976  lmbrf  16992  cncnp  17011  lmss  17028  isnrm2  17088  cmpfi  17137  1stcfb  17173  1stccnp  17190  ptrescn  17335  txkgen  17348  xkoinjcn  17383  trfil3  17585  fmid  17657  lmflf  17702  txflf  17703  ptcmplem3  17750  tsmsf1o  17829  metrest  18072  metcnp  18089  metcnp2  18090  txmetcnp  18095  evth2  18460  lmmbrf  18690  iscfil2  18694  fmcfil  18700  iscau2  18705  iscau4  18707  iscauf  18708  caucfil  18711  iscmet3lem3  18718  cfilresi  18723  causs  18726  lmclim  18730  ivth2  18817  ovolfioo  18829  ovolficc  18830  ovolshftlem1  18870  ovolscalem1  18874  volsup2  18962  ismbf3d  19011  mbfaddlem  19017  mbfsup  19021  mbfinf  19022  itg2seq  19099  itg2gt0  19117  ellimc2  19229  ellimc3  19231  rolle  19339  cmvth  19340  mvth  19341  dvlip  19342  dvivth  19359  lhop1lem  19362  deg1ldg  19480  ulm2  19766  ulmdvlem3  19781  dcubic  20144  mcubic  20145  cubic2  20146  rlimcnp  20262  ftalem3  20314  isppw2  20355  lgsquadlem2  20596  dchrmusumlema  20644  dchrisum0lema  20665  nmobndi  21355  nmounbi  21356  nmoo0  21371  h2hcau  21561  h2hlm  21562  shsel3  21896  pjhtheu2  21997  chscllem2  22219  adjbdln  22665  branmfn  22687  pjimai  22758  chrelati  22946  cdj3lem3  23020  cdj3lem3b  23022  dfimafnf  23043  ballotlemodife  23058  lmdvg  23378  gsumpropd2lem  23381  erdszelem10  23733  iscvm  23792  elfuns  24456  axsegcon  24557  axpasch  24571  axcontlem7  24600  seglelin  24741  outsideofeu  24756  supadd  24928  prl2  25180  prjmapcp2  25181  iscst4  25188  nZdef  25191  prodeq3ii  25319  osneisi  25542  bwt2  25603  lvsovso2  25638  supnuf  25640  supexr  25642  cnegvex2  25671  rnegvex2  25672  fnckle  26056  bhp2a  26187  opnrebl  26246  opnrebl2  26247  filnetlem4  26341  lmclim2  26485  caures  26487  isbnd3b  26520  heiborlem7  26552  heiborlem10  26555  rrncmslem  26567  isdrngo2  26600  prter3  26761  elrfirn  26781  elrfirn2  26782  mrefg3  26794  diophin  26863  diophun  26864  diophren  26907  rmxycomplete  27013  wepwsolem  27149  fnwe2lem2  27159  islssfg  27179  elfilspd  27266  dfaimafn  28038  islshpsm  29243  lsatfixedN  29272  lrelat  29277  eqlkr2  29363  lshpkrlem1  29373  lfl1dim  29384  eqlkr4  29428  ishlat3N  29617  hlsupr2  29649  hlrelat5N  29663  hlrelat  29664  cvrval5  29677  cvrat42  29706  athgt  29718  3dim0  29719  islln3  29772  llnexatN  29783  islpln3  29795  islvol3  29838  islvol5  29841  isline4N  30039  polval2N  30168  4atex3  30343  cdleme0ex2N  30486  cdlemefrs29cpre1  30660  cdlemb3  30868  cdlemg33c  30970  cdlemg33e  30972  dia1dim2  31325  cdlemm10N  31381  dib1dim2  31431  diclspsn  31457  dih1dimatlem  31592  dihatexv2  31602  djhcvat42  31678  dihjat1lem  31691  dvh4dimat  31701  dvh2dimatN  31703  lcfrlem9  31813  mapdval4N  31895  mapdcv  31923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-nf 1534  df-rex 2551
  Copyright terms: Public domain W3C validator