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

Theorem rexlimdvaa 2915
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 618 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2914 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   E.wrex 2772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2776  df-rex 2777
This theorem is referenced by:  rexlimddv  2918  tz7.7  5468  isofrlem  6246  nnawordex  7349  oaabs2  7357  fiin  7945  marypha1lem  7956  wemaplem3  8072  cantnflt  8185  fseqenlem2  8463  cardaleph  8527  coftr  8710  fin23lem26  8762  fin1a2lem13  8849  fpwwe2  9075  r1wunlim  9169  wunex2  9170  inttsk  9206  grur1  9252  inaprc  9268  receu  10264  zsupss  11260  xralrple  11505  rexanuz  13408  limsupval2  13539  limsupval2OLD  13540  caucvgb  13745  fsumiun  13880  rpnnen2  14277  dvdsval2  14307  prmind2  14634  pcprmpw2  14830  pockthg  14849  prmreclem5  14863  vdwlem6  14935  vdwlem10  14939  sscpwex  15719  drsdirfi  16182  psgnunilem3  17136  sylow3lem2  17279  efgsfo  17388  lt6abl  17528  ghmcyg  17529  unitgrp  17894  irredrmul  17934  drngnidl  18452  znunit  19132  tgcl  19983  neiint  20118  restopnb  20189  ordtrest2lem  20217  pnfnei  20234  mnfnei  20235  iscnp4  20277  haust1  20366  ordthauslem  20397  tgcmp  20414  t1conperf  20449  2ndc1stc  20464  2ndcdisj  20469  islly2  20497  nllyrest  20499  reftr  20527  comppfsc  20545  ptbasfi  20594  ptcnp  20635  xkococnlem  20672  tgqtop  20725  fbssfi  20850  fgabs  20892  neifil  20893  trfil2  20900  elfm2  20961  elfm3  20963  rnelfmlem  20965  fmfnfmlem4  20970  flffbas  21008  fclsfnflim  21040  ptcmplem4  21068  tsmsxp  21167  blssexps  21439  blssex  21440  icccmplem3  21840  cnheibor  21981  pi1blem  22068  iscfil3  22241  iscmet3lem2  22260  cmetss  22282  ovolicc2  22474  nulmbl2  22488  volsup  22507  dyadmbllem  22555  itg2const2  22697  bddmulibl  22794  limcflf  22834  itgsubst  22999  ulmdvlem3  23355  xrlimcnp  23892  amgm  23914  dchrptlem2  24191  lgsne0  24259  lgsqr  24272  lgsquadlem1  24280  dchrvmasumif  24339  rpvmasum2  24348  dchrisum0re  24349  dchrisum0lem3  24355  dchrisum0  24356  dchrmusum  24360  dchrvmasum  24361  chpdifbnd  24391  pntrlog2bnd  24420  pntibndlem3  24428  pntibnd  24429  pntleml  24447  ostth  24475  brbtwn2  24933  colinearalg  24938  cusgrafilem1  25205  nmobndi  26414  spansneleq  27221  ofrn2  28243  xreceu  28398  ordtrest2NEWlem  28736  dya2iocnei  29112  conpcon  29966  cvmsss2  30005  cvmlift2lem10  30043  cvmlift3lem2  30051  nodenselem5  30579  nobndlem6  30591  outsidele  30904  neibastop1  31020  neibastop2lem  31021  mblfinlem1  31941  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  cnambfre  31953  itg2addnclem  31957  itg2addnclem3  31959  bddiblnc  31976  ftc1anclem7  31987  ftc1anc  31989  fdc  32038  sstotbnd2  32070  sstotbnd  32071  isbndx  32078  ssbnd  32084  totbndbnd  32085  heibor  32117  unichnidl  32228  pexmidlem8N  33511  elrfi  35505  fnwe2lem2  35879  hbtlem5  35957  nbusgrvtx  39180  cusgrfilem1  39272  2zrngamgm  39558
  Copyright terms: Public domain W3C validator