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 615 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2836 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  rexlimddv  2840  tz7.7  4740  isofrlem  6026  nnawordex  7068  oaabs2  7076  fiin  7664  marypha1lem  7675  wemaplem3  7754  cantnflt  7872  cantnfltOLD  7902  fseqenlem2  8187  cardaleph  8251  coftr  8434  fin23lem26  8486  fin1a2lem13  8573  fpwwe2  8802  r1wunlim  8896  wunex2  8897  inttsk  8933  grur1  8979  inaprc  8995  receu  9973  zsupss  10936  xralrple  11167  rexanuz  12825  limsupval2  12950  caucvgb  13149  fsumiun  13276  rpnnen2  13500  dvdsval2  13530  prmind2  13766  pcprmpw2  13940  pockthg  13959  prmreclem5  13973  vdwlem6  14039  vdwlem10  14043  sscpwex  14720  drsdirfi  15100  psgnunilem3  15993  sylow3lem2  16118  efgsfo  16227  lt6abl  16362  ghmcyg  16363  unitgrp  16747  irredrmul  16787  drngnidl  17288  znunit  17971  tgcl  18549  neiint  18683  restopnb  18754  ordtrest2lem  18782  pnfnei  18799  mnfnei  18800  iscnp4  18842  haust1  18931  ordthauslem  18962  tgcmp  18979  t1conperf  19015  2ndc1stc  19030  2ndcdisj  19035  islly2  19063  nllyrest  19065  ptbasfi  19129  ptcnp  19170  xkococnlem  19207  tgqtop  19260  fbssfi  19385  fgabs  19427  neifil  19428  trfil2  19435  elfm2  19496  elfm3  19498  rnelfmlem  19500  fmfnfmlem4  19505  flffbas  19543  fclsfnflim  19575  ptcmplem4  19602  tsmsxp  19704  blssexps  19976  blssex  19977  icccmplem3  20376  cnheibor  20502  pi1blem  20586  iscfil3  20759  iscmet3lem2  20778  cmetss  20800  ovolicc2  20980  nulmbl2  20993  volsup  21012  dyadmbllem  21054  itg2const2  21194  bddmulibl  21291  limcflf  21331  itgsubst  21496  ulmdvlem3  21842  xrlimcnp  22337  amgm  22359  dchrptlem2  22579  lgsne0  22647  lgsqr  22660  lgsquadlem1  22668  dchrvmasumif  22727  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lem3  22743  dchrisum0  22744  dchrmusum  22748  dchrvmasum  22749  chpdifbnd  22779  pntrlog2bnd  22808  pntibndlem3  22816  pntibnd  22817  pntleml  22835  ostth  22863  brbtwn2  23102  colinearalg  23107  cusgrafilem1  23338  nmobndi  24126  spansneleq  24924  ofrn2  25909  xreceu  26048  ordtrest2NEWlem  26304  dya2iocnei  26649  conpcon  27076  cvmsss2  27115  cvmlift2lem10  27153  cvmlift3lem2  27161  nodenselem5  27777  nobndlem6  27789  outsidele  28114  mblfinlem1  28381  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  cnambfre  28393  itg2addnclem  28396  itg2addnclem3  28398  bddiblnc  28415  ftc1anclem7  28426  ftc1anc  28428  reftr  28514  comppfsc  28532  neibastop1  28533  neibastop2lem  28534  fdc  28594  sstotbnd2  28626  sstotbnd  28627  isbndx  28634  ssbnd  28640  totbndbnd  28641  heibor  28673  unichnidl  28784  elrfi  28983  fnwe2lem2  29357  hbtlem5  29437  pexmidlem8N  33461
  Copyright terms: Public domain W3C validator