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

Theorem rexlimdvaa 2936
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 2935 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  rexlimddv  2939  tz7.7  4894  isofrlem  6221  nnawordex  7288  oaabs2  7296  fiin  7884  marypha1lem  7895  wemaplem3  7976  cantnflt  8094  cantnfltOLD  8124  fseqenlem2  8409  cardaleph  8473  coftr  8656  fin23lem26  8708  fin1a2lem13  8795  fpwwe2  9024  r1wunlim  9118  wunex2  9119  inttsk  9155  grur1  9201  inaprc  9217  receu  10201  zsupss  11181  xralrple  11414  rexanuz  13159  limsupval2  13284  caucvgb  13483  fsumiun  13616  rpnnen2  13940  dvdsval2  13970  prmind2  14209  pcprmpw2  14386  pockthg  14405  prmreclem5  14419  vdwlem6  14485  vdwlem10  14489  sscpwex  15165  drsdirfi  15545  psgnunilem3  16499  sylow3lem2  16626  efgsfo  16735  lt6abl  16875  ghmcyg  16876  unitgrp  17294  irredrmul  17334  drngnidl  17855  znunit  18579  tgcl  19448  neiint  19582  restopnb  19653  ordtrest2lem  19681  pnfnei  19698  mnfnei  19699  iscnp4  19741  haust1  19830  ordthauslem  19861  tgcmp  19878  t1conperf  19914  2ndc1stc  19929  2ndcdisj  19934  islly2  19962  nllyrest  19964  reftr  19992  comppfsc  20010  ptbasfi  20059  ptcnp  20100  xkococnlem  20137  tgqtop  20190  fbssfi  20315  fgabs  20357  neifil  20358  trfil2  20365  elfm2  20426  elfm3  20428  rnelfmlem  20430  fmfnfmlem4  20435  flffbas  20473  fclsfnflim  20505  ptcmplem4  20532  tsmsxp  20634  blssexps  20906  blssex  20907  icccmplem3  21306  cnheibor  21432  pi1blem  21516  iscfil3  21689  iscmet3lem2  21708  cmetss  21730  ovolicc2  21910  nulmbl2  21924  volsup  21943  dyadmbllem  21985  itg2const2  22125  bddmulibl  22222  limcflf  22262  itgsubst  22427  ulmdvlem3  22773  xrlimcnp  23274  amgm  23296  dchrptlem2  23516  lgsne0  23584  lgsqr  23597  lgsquadlem1  23605  dchrvmasumif  23664  rpvmasum2  23673  dchrisum0re  23674  dchrisum0lem3  23680  dchrisum0  23681  dchrmusum  23685  dchrvmasum  23686  chpdifbnd  23716  pntrlog2bnd  23745  pntibndlem3  23753  pntibnd  23754  pntleml  23772  ostth  23800  brbtwn2  24184  colinearalg  24189  cusgrafilem1  24455  nmobndi  25666  spansneleq  26464  ofrn2  27456  xreceu  27595  ordtrest2NEWlem  27881  dya2iocnei  28230  conpcon  28657  cvmsss2  28696  cvmlift2lem10  28734  cvmlift3lem2  28742  nodenselem5  29420  nobndlem6  29432  outsidele  29757  mblfinlem1  30026  mblfinlem3  30028  mblfinlem4  30029  ismblfin  30030  cnambfre  30038  itg2addnclem  30041  itg2addnclem3  30043  bddiblnc  30060  ftc1anclem7  30071  ftc1anc  30073  neibastop1  30152  neibastop2lem  30153  fdc  30213  sstotbnd2  30245  sstotbnd  30246  isbndx  30253  ssbnd  30259  totbndbnd  30260  heibor  30292  unichnidl  30403  elrfi  30601  fnwe2lem2  30972  hbtlem5  31052  2zrngamgm  32455  pexmidlem8N  35441
  Copyright terms: Public domain W3C validator