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

Theorem rexlimdvaa 2949
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypothesis
Ref Expression
rexlimdvaa.1  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
Assertion
Ref Expression
rexlimdvaa  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdvaa
StepHypRef Expression
1 rexlimdvaa.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
21expr 615 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2948 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-ral 2812  df-rex 2813
This theorem is referenced by:  rexlimddv  2952  tz7.7  4897  isofrlem  6215  nnawordex  7276  oaabs2  7284  fiin  7871  marypha1lem  7882  wemaplem3  7962  cantnflt  8080  cantnfltOLD  8110  fseqenlem2  8395  cardaleph  8459  coftr  8642  fin23lem26  8694  fin1a2lem13  8781  fpwwe2  9010  r1wunlim  9104  wunex2  9105  inttsk  9141  grur1  9187  inaprc  9203  receu  10183  zsupss  11160  xralrple  11393  rexanuz  13127  limsupval2  13252  caucvgb  13451  fsumiun  13584  rpnnen2  13809  dvdsval2  13839  prmind2  14076  pcprmpw2  14253  pockthg  14272  prmreclem5  14286  vdwlem6  14352  vdwlem10  14356  sscpwex  15034  drsdirfi  15414  psgnunilem3  16310  sylow3lem2  16437  efgsfo  16546  lt6abl  16681  ghmcyg  16682  unitgrp  17093  irredrmul  17133  drngnidl  17652  znunit  18362  tgcl  19230  neiint  19364  restopnb  19435  ordtrest2lem  19463  pnfnei  19480  mnfnei  19481  iscnp4  19523  haust1  19612  ordthauslem  19643  tgcmp  19660  t1conperf  19696  2ndc1stc  19711  2ndcdisj  19716  islly2  19744  nllyrest  19746  ptbasfi  19810  ptcnp  19851  xkococnlem  19888  tgqtop  19941  fbssfi  20066  fgabs  20108  neifil  20109  trfil2  20116  elfm2  20177  elfm3  20179  rnelfmlem  20181  fmfnfmlem4  20186  flffbas  20224  fclsfnflim  20256  ptcmplem4  20283  tsmsxp  20385  blssexps  20657  blssex  20658  icccmplem3  21057  cnheibor  21183  pi1blem  21267  iscfil3  21440  iscmet3lem2  21459  cmetss  21481  ovolicc2  21661  nulmbl2  21675  volsup  21694  dyadmbllem  21736  itg2const2  21876  bddmulibl  21973  limcflf  22013  itgsubst  22178  ulmdvlem3  22524  xrlimcnp  23019  amgm  23041  dchrptlem2  23261  lgsne0  23329  lgsqr  23342  lgsquadlem1  23350  dchrvmasumif  23409  rpvmasum2  23418  dchrisum0re  23419  dchrisum0lem3  23425  dchrisum0  23426  dchrmusum  23430  dchrvmasum  23431  chpdifbnd  23461  pntrlog2bnd  23490  pntibndlem3  23498  pntibnd  23499  pntleml  23517  ostth  23545  brbtwn2  23877  colinearalg  23882  cusgrafilem1  24141  nmobndi  25352  spansneleq  26150  ofrn2  27139  xreceu  27272  ordtrest2NEWlem  27526  dya2iocnei  27879  conpcon  28306  cvmsss2  28345  cvmlift2lem10  28383  cvmlift3lem2  28391  nodenselem5  29008  nobndlem6  29020  outsidele  29345  mblfinlem1  29615  mblfinlem3  29617  mblfinlem4  29618  ismblfin  29619  cnambfre  29627  itg2addnclem  29630  itg2addnclem3  29632  bddiblnc  29649  ftc1anclem7  29660  ftc1anc  29662  reftr  29748  comppfsc  29766  neibastop1  29767  neibastop2lem  29768  fdc  29828  sstotbnd2  29860  sstotbnd  29861  isbndx  29868  ssbnd  29874  totbndbnd  29875  heibor  29907  unichnidl  30018  elrfi  30217  fnwe2lem2  30590  hbtlem5  30670  pexmidlem8N  34648
  Copyright terms: Public domain W3C validator