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

Theorem rexlimdvaa 2837
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 600 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2836 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1727   E.wrex 2712
This theorem is referenced by:  rexlimddv  2840  tz7.7  4636  isofrlem  6089  nnawordex  6909  oaabs2  6917  fiin  7456  marypha1lem  7467  wemaplem3  7546  cantnflt  7656  fseqenlem2  7937  cardaleph  8001  coftr  8184  fin23lem26  8236  fin1a2lem13  8323  fpwwe2  8549  r1wunlim  8643  wunex2  8644  inttsk  8680  grur1  8726  inaprc  8742  receu  9698  zsupss  10596  xralrple  10822  rexanuz  12180  limsupval2  12305  caucvgb  12504  fsumiun  12631  rpnnen2  12856  dvdsval2  12886  prmind2  13121  pcprmpw2  13286  pockthg  13305  prmreclem5  13319  vdwlem6  13385  vdwlem10  13389  sscpwex  14046  drsdirfi  14426  sylow3lem2  15293  efgsfo  15402  lt6abl  15535  ghmcyg  15536  unitgrp  15803  irredrmul  15843  drngnidl  16331  znunit  16875  tgcl  17065  neiint  17199  restopnb  17270  ordtrest2lem  17298  pnfnei  17315  mnfnei  17316  iscnp4  17358  haust1  17447  ordthauslem  17478  tgcmp  17495  t1conperf  17530  2ndc1stc  17545  2ndcdisj  17550  islly2  17578  nllyrest  17580  ptbasfi  17644  ptcnp  17685  xkococnlem  17722  tgqtop  17775  fbssfi  17900  fgabs  17942  neifil  17943  trfil2  17950  elfm2  18011  elfm3  18013  rnelfmlem  18015  fmfnfmlem4  18020  flffbas  18058  fclsfnflim  18090  ptcmplem4  18117  tsmsxp  18215  blssexps  18487  blssex  18488  icccmplem3  18886  cnheibor  19011  pi1blem  19095  iscfil3  19257  iscmet3lem2  19276  cmetss  19298  ovolicc2  19449  nulmbl2  19462  volsup  19481  dyadmbllem  19522  itg2const2  19662  bddmulibl  19759  limcflf  19799  itgsubst  19964  ulmdvlem3  20349  xrlimcnp  20838  amgm  20860  dchrptlem2  21080  lgsne0  21148  lgsqr  21161  lgsquadlem1  21169  dchrvmasumif  21228  rpvmasum2  21237  dchrisum0re  21238  dchrisum0lem3  21244  dchrisum0  21245  dchrmusum  21249  dchrvmasum  21250  chpdifbnd  21280  pntrlog2bnd  21309  pntibndlem3  21317  pntibnd  21318  pntleml  21336  ostth  21364  cusgrafilem1  21519  nmobndi  22307  spansneleq  23103  ofrn2  24084  xreceu  24199  dya2iocnei  24663  conpcon  24953  cvmsss2  24992  cvmlift2lem10  25030  cvmlift3lem2  25038  nodenselem5  25671  nobndlem6  25683  brbtwn2  25875  colinearalg  25880  outsidele  26097  mblfinlem1  26279  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  cnambfre  26291  itg2addnclem  26294  itg2addnclem3  26296  bddiblnc  26313  ftc1anclem7  26324  ftc1anc  26326  reftr  26407  comppfsc  26425  neibastop1  26426  neibastop2lem  26427  fdc  26487  sstotbnd2  26521  sstotbnd  26522  isbndx  26529  ssbnd  26535  totbndbnd  26536  heibor  26568  unichnidl  26679  elrfi  26786  fnwe2lem2  27164  hbtlem5  27347  psgnunilem3  27434  pexmidlem8N  30872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2716  df-rex 2717
  Copyright terms: Public domain W3C validator