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

Theorem rexlimdvaa 2823
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 2822 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  rexlimddv  2826  tz7.7  4599  isofrlem  6052  nnawordex  6872  oaabs2  6880  fiin  7419  marypha1lem  7430  wemaplem3  7509  cantnflt  7619  fseqenlem2  7898  cardaleph  7962  coftr  8145  fin23lem26  8197  fin1a2lem13  8284  fpwwe2  8510  r1wunlim  8604  wunex2  8605  inttsk  8641  grur1  8687  inaprc  8703  receu  9659  zsupss  10557  xralrple  10783  rexanuz  12141  limsupval2  12266  caucvgb  12465  fsumiun  12592  rpnnen2  12817  dvdsval2  12847  prmind2  13082  pcprmpw2  13247  pockthg  13266  prmreclem5  13280  vdwlem6  13346  vdwlem10  13350  sscpwex  14007  drsdirfi  14387  sylow3lem2  15254  efgsfo  15363  lt6abl  15496  ghmcyg  15497  unitgrp  15764  irredrmul  15804  drngnidl  16292  znunit  16836  tgcl  17026  neiint  17160  restopnb  17231  ordtrest2lem  17259  pnfnei  17276  mnfnei  17277  iscnp4  17319  haust1  17408  ordthauslem  17439  tgcmp  17456  t1conperf  17491  2ndc1stc  17506  2ndcdisj  17511  islly2  17539  nllyrest  17541  ptbasfi  17605  ptcnp  17646  xkococnlem  17683  tgqtop  17736  fbssfi  17861  fgabs  17903  neifil  17904  trfil2  17911  elfm2  17972  elfm3  17974  rnelfmlem  17976  fmfnfmlem4  17981  flffbas  18019  fclsfnflim  18051  ptcmplem4  18078  tsmsxp  18176  blssexps  18448  blssex  18449  icccmplem3  18847  cnheibor  18972  pi1blem  19056  iscfil3  19218  iscmet3lem2  19237  cmetss  19259  ovolicc2  19410  nulmbl2  19423  volsup  19442  dyadmbllem  19483  itg2const2  19625  bddmulibl  19722  limcflf  19760  itgsubst  19925  ulmdvlem3  20310  xrlimcnp  20799  amgm  20821  dchrptlem2  21041  lgsne0  21109  lgsqr  21122  lgsquadlem1  21130  dchrvmasumif  21189  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem3  21205  dchrisum0  21206  dchrmusum  21210  dchrvmasum  21211  chpdifbnd  21241  pntrlog2bnd  21270  pntibndlem3  21278  pntibnd  21279  pntleml  21297  ostth  21325  cusgrafilem1  21480  nmobndi  22268  spansneleq  23064  ofrn2  24045  xreceu  24160  dya2iocnei  24624  conpcon  24914  cvmsss2  24953  cvmlift2lem10  24991  cvmlift3lem2  24999  nodenselem5  25632  nobndlem6  25644  brbtwn2  25836  colinearalg  25841  outsidele  26058  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  cnambfre  26245  itg2addnclem  26246  itg2addnclem3  26248  bddiblnc  26265  ftc1anclem7  26276  ftc1anc  26278  reftr  26360  comppfsc  26378  neibastop1  26379  neibastop2lem  26380  fdc  26440  sstotbnd2  26474  sstotbnd  26475  isbndx  26482  ssbnd  26488  totbndbnd  26489  heibor  26521  unichnidl  26632  elrfi  26739  fnwe2lem2  27117  hbtlem5  27300  psgnunilem3  27387  pexmidlem8N  30711
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator