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

Theorem rexlimdvaa 2875
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 613 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2874 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1826   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-ral 2737  df-rex 2738
This theorem is referenced by:  rexlimddv  2878  tz7.7  4818  isofrlem  6137  nnawordex  7204  oaabs2  7212  fiin  7797  marypha1lem  7808  wemaplem3  7888  cantnflt  8004  cantnfltOLD  8034  fseqenlem2  8319  cardaleph  8383  coftr  8566  fin23lem26  8618  fin1a2lem13  8705  fpwwe2  8932  r1wunlim  9026  wunex2  9027  inttsk  9063  grur1  9109  inaprc  9125  receu  10111  zsupss  11090  xralrple  11325  rexanuz  13180  limsupval2  13305  caucvgb  13504  fsumiun  13637  rpnnen2  13961  dvdsval2  13991  prmind2  14230  pcprmpw2  14407  pockthg  14426  prmreclem5  14440  vdwlem6  14506  vdwlem10  14510  sscpwex  15221  drsdirfi  15684  psgnunilem3  16638  sylow3lem2  16765  efgsfo  16874  lt6abl  17014  ghmcyg  17015  unitgrp  17429  irredrmul  17469  drngnidl  17990  znunit  18693  tgcl  19556  neiint  19691  restopnb  19762  ordtrest2lem  19790  pnfnei  19807  mnfnei  19808  iscnp4  19850  haust1  19939  ordthauslem  19970  tgcmp  19987  t1conperf  20022  2ndc1stc  20037  2ndcdisj  20042  islly2  20070  nllyrest  20072  reftr  20100  comppfsc  20118  ptbasfi  20167  ptcnp  20208  xkococnlem  20245  tgqtop  20298  fbssfi  20423  fgabs  20465  neifil  20466  trfil2  20473  elfm2  20534  elfm3  20536  rnelfmlem  20538  fmfnfmlem4  20543  flffbas  20581  fclsfnflim  20613  ptcmplem4  20640  tsmsxp  20742  blssexps  21014  blssex  21015  icccmplem3  21414  cnheibor  21540  pi1blem  21624  iscfil3  21797  iscmet3lem2  21816  cmetss  21838  ovolicc2  22018  nulmbl2  22032  volsup  22051  dyadmbllem  22093  itg2const2  22233  bddmulibl  22330  limcflf  22370  itgsubst  22535  ulmdvlem3  22882  xrlimcnp  23415  amgm  23437  dchrptlem2  23657  lgsne0  23725  lgsqr  23738  lgsquadlem1  23746  dchrvmasumif  23805  rpvmasum2  23814  dchrisum0re  23815  dchrisum0lem3  23821  dchrisum0  23822  dchrmusum  23826  dchrvmasum  23827  chpdifbnd  23857  pntrlog2bnd  23886  pntibndlem3  23894  pntibnd  23895  pntleml  23913  ostth  23941  brbtwn2  24329  colinearalg  24334  cusgrafilem1  24600  nmobndi  25807  spansneleq  26605  ofrn2  27620  xreceu  27771  ordtrest2NEWlem  28058  dya2iocnei  28409  conpcon  28869  cvmsss2  28908  cvmlift2lem10  28946  cvmlift3lem2  28954  nodenselem5  29610  nobndlem6  29622  outsidele  29935  mblfinlem1  30216  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  cnambfre  30228  itg2addnclem  30232  itg2addnclem3  30234  bddiblnc  30251  ftc1anclem7  30262  ftc1anc  30264  neibastop1  30343  neibastop2lem  30344  fdc  30404  sstotbnd2  30436  sstotbnd  30437  isbndx  30444  ssbnd  30450  totbndbnd  30451  heibor  30483  unichnidl  30594  elrfi  30792  fnwe2lem2  31163  hbtlem5  31245  2zrngamgm  32945  pexmidlem8N  36114
  Copyright terms: Public domain W3C validator