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

Theorem rexlimdvaa 2791
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 599 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2790 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  rexlimddv  2794  tz7.7  4567  isofrlem  6019  nnawordex  6839  oaabs2  6847  fiin  7385  marypha1lem  7396  wemaplem3  7473  cantnflt  7583  fseqenlem2  7862  cardaleph  7926  coftr  8109  fin23lem26  8161  fin1a2lem13  8248  fpwwe2  8474  r1wunlim  8568  wunex2  8569  inttsk  8605  grur1  8651  inaprc  8667  receu  9623  zsupss  10521  xralrple  10747  rexanuz  12104  limsupval2  12229  caucvgb  12428  fsumiun  12555  rpnnen2  12780  dvdsval2  12810  prmind2  13045  pcprmpw2  13210  pockthg  13229  prmreclem5  13243  vdwlem6  13309  vdwlem10  13313  sscpwex  13970  drsdirfi  14350  sylow3lem2  15217  efgsfo  15326  lt6abl  15459  ghmcyg  15460  unitgrp  15727  irredrmul  15767  drngnidl  16255  znunit  16799  tgcl  16989  neiint  17123  restopnb  17193  ordtrest2lem  17221  pnfnei  17238  mnfnei  17239  iscnp4  17281  haust1  17370  ordthauslem  17401  tgcmp  17418  t1conperf  17452  2ndc1stc  17467  2ndcdisj  17472  islly2  17500  nllyrest  17502  ptbasfi  17566  ptcnp  17607  xkococnlem  17644  tgqtop  17697  fbssfi  17822  fgabs  17864  neifil  17865  trfil2  17872  elfm2  17933  elfm3  17935  rnelfmlem  17937  fmfnfmlem4  17942  flffbas  17980  fclsfnflim  18012  ptcmplem4  18039  tsmsxp  18137  blssexps  18409  blssex  18410  icccmplem3  18808  cnheibor  18933  pi1blem  19017  iscfil3  19179  iscmet3lem2  19198  cmetss  19220  ovolicc2  19371  nulmbl2  19384  volsup  19403  dyadmbllem  19444  itg2const2  19586  bddmulibl  19683  limcflf  19721  itgsubst  19886  ulmdvlem3  20271  xrlimcnp  20760  amgm  20782  dchrptlem2  21002  lgsne0  21070  lgsqr  21083  lgsquadlem1  21091  dchrvmasumif  21150  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  dchrmusum  21171  dchrvmasum  21172  chpdifbnd  21202  pntrlog2bnd  21231  pntibndlem3  21239  pntibnd  21240  pntleml  21258  ostth  21286  cusgrafilem1  21441  nmobndi  22229  spansneleq  23025  ofrn2  24006  xreceu  24121  dya2iocnei  24585  conpcon  24875  cvmsss2  24914  cvmlift2lem10  24952  cvmlift3lem2  24960  nodenselem5  25553  nobndlem6  25565  brbtwn2  25748  colinearalg  25753  outsidele  25970  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  cnambfre  26154  itg2addnclem  26155  itg2addnclem3  26157  bddiblnc  26174  reftr  26259  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  fdc  26339  sstotbnd2  26373  sstotbnd  26374  isbndx  26381  ssbnd  26387  totbndbnd  26388  heibor  26420  unichnidl  26531  elrfi  26638  fnwe2lem2  27016  hbtlem5  27200  psgnunilem3  27287  pexmidlem8N  30459
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 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator