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

Theorem rexlimdvaa 2892
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 624 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2891 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   E.wrex 2750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755
This theorem is referenced by:  rexlimddv  2895  tz7.7  5472  isofrlem  6261  nnawordex  7369  oaabs2  7377  fiin  7967  marypha1lem  7978  wemaplem3  8094  cantnflt  8208  fseqenlem2  8487  cardaleph  8551  coftr  8734  fin23lem26  8786  fin1a2lem13  8873  fpwwe2  9099  r1wunlim  9193  wunex2  9194  inttsk  9230  grur1  9276  inaprc  9292  receu  10290  zsupss  11287  xralrple  11532  rexanuz  13463  limsupval2  13595  limsupval2OLD  13596  caucvgb  13801  fsumiun  13936  rpnnen2  14333  dvdsval2  14363  prmind2  14690  pcprmpw2  14886  pockthg  14905  prmreclem5  14919  vdwlem6  14991  vdwlem10  14995  sscpwex  15775  drsdirfi  16238  psgnunilem3  17192  sylow3lem2  17335  efgsfo  17444  lt6abl  17584  ghmcyg  17585  unitgrp  17950  irredrmul  17990  drngnidl  18508  znunit  19189  tgcl  20040  neiint  20175  restopnb  20246  ordtrest2lem  20274  pnfnei  20291  mnfnei  20292  iscnp4  20334  haust1  20423  ordthauslem  20454  tgcmp  20471  t1conperf  20506  2ndc1stc  20521  2ndcdisj  20526  islly2  20554  nllyrest  20556  reftr  20584  comppfsc  20602  ptbasfi  20651  ptcnp  20692  xkococnlem  20729  tgqtop  20782  fbssfi  20907  fgabs  20949  neifil  20950  trfil2  20957  elfm2  21018  elfm3  21020  rnelfmlem  21022  fmfnfmlem4  21027  flffbas  21065  fclsfnflim  21097  ptcmplem4  21125  tsmsxp  21224  blssexps  21496  blssex  21497  icccmplem3  21897  cnheibor  22038  pi1blem  22125  iscfil3  22298  iscmet3lem2  22317  cmetss  22339  ovolicc2  22531  nulmbl2  22545  volsup  22565  dyadmbllem  22613  itg2const2  22755  bddmulibl  22852  limcflf  22892  itgsubst  23057  ulmdvlem3  23413  xrlimcnp  23950  amgm  23972  dchrptlem2  24249  lgsne0  24317  lgsqr  24330  lgsquadlem1  24338  dchrvmasumif  24397  rpvmasum2  24406  dchrisum0re  24407  dchrisum0lem3  24413  dchrisum0  24414  dchrmusum  24418  dchrvmasum  24419  chpdifbnd  24449  pntrlog2bnd  24478  pntibndlem3  24486  pntibnd  24487  pntleml  24505  ostth  24533  brbtwn2  24991  colinearalg  24996  cusgrafilem1  25263  nmobndi  26472  spansneleq  27279  ofrn2  28294  xreceu  28443  ordtrest2NEWlem  28779  dya2iocnei  29154  conpcon  30008  cvmsss2  30047  cvmlift2lem10  30085  cvmlift3lem2  30093  nodenselem5  30624  nobndlem6  30636  outsidele  30949  neibastop1  31065  neibastop2lem  31066  mblfinlem1  32023  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  cnambfre  32035  itg2addnclem  32039  itg2addnclem3  32041  bddiblnc  32058  ftc1anclem7  32069  ftc1anc  32071  fdc  32120  sstotbnd2  32152  sstotbnd  32153  isbndx  32160  ssbnd  32166  totbndbnd  32167  heibor  32199  unichnidl  32310  pexmidlem8N  33588  elrfi  35582  fnwe2lem2  35955  hbtlem5  36033  nbumgrvtx  39560  cusgrfilem1  39662  2zrngamgm  40308
  Copyright terms: Public domain W3C validator