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

Theorem rexlimdvaa 2832
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 610 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2831 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  rexlimddv  2835  tz7.7  4732  isofrlem  6018  nnawordex  7064  oaabs2  7072  fiin  7660  marypha1lem  7671  wemaplem3  7750  cantnflt  7868  cantnfltOLD  7898  fseqenlem2  8183  cardaleph  8247  coftr  8430  fin23lem26  8482  fin1a2lem13  8569  fpwwe2  8798  r1wunlim  8892  wunex2  8893  inttsk  8929  grur1  8975  inaprc  8991  receu  9969  zsupss  10932  xralrple  11163  rexanuz  12817  limsupval2  12942  caucvgb  13141  fsumiun  13267  rpnnen2  13491  dvdsval2  13521  prmind2  13757  pcprmpw2  13931  pockthg  13950  prmreclem5  13964  vdwlem6  14030  vdwlem10  14034  sscpwex  14711  drsdirfi  15091  psgnunilem3  15982  sylow3lem2  16107  efgsfo  16216  lt6abl  16351  ghmcyg  16352  unitgrp  16693  irredrmul  16733  drngnidl  17233  znunit  17838  tgcl  18416  neiint  18550  restopnb  18621  ordtrest2lem  18649  pnfnei  18666  mnfnei  18667  iscnp4  18709  haust1  18798  ordthauslem  18829  tgcmp  18846  t1conperf  18882  2ndc1stc  18897  2ndcdisj  18902  islly2  18930  nllyrest  18932  ptbasfi  18996  ptcnp  19037  xkococnlem  19074  tgqtop  19127  fbssfi  19252  fgabs  19294  neifil  19295  trfil2  19302  elfm2  19363  elfm3  19365  rnelfmlem  19367  fmfnfmlem4  19372  flffbas  19410  fclsfnflim  19442  ptcmplem4  19469  tsmsxp  19571  blssexps  19843  blssex  19844  icccmplem3  20243  cnheibor  20369  pi1blem  20453  iscfil3  20626  iscmet3lem2  20645  cmetss  20667  ovolicc2  20847  nulmbl2  20860  volsup  20879  dyadmbllem  20921  itg2const2  21061  bddmulibl  21158  limcflf  21198  itgsubst  21363  ulmdvlem3  21752  xrlimcnp  22247  amgm  22269  dchrptlem2  22489  lgsne0  22557  lgsqr  22570  lgsquadlem1  22578  dchrvmasumif  22637  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lem3  22653  dchrisum0  22654  dchrmusum  22658  dchrvmasum  22659  chpdifbnd  22689  pntrlog2bnd  22718  pntibndlem3  22726  pntibnd  22727  pntleml  22745  ostth  22773  brbtwn2  22974  colinearalg  22979  cusgrafilem1  23210  nmobndi  23998  spansneleq  24796  ofrn2  25782  xreceu  25920  ordtrest2NEWlem  26206  dya2iocnei  26551  conpcon  26972  cvmsss2  27011  cvmlift2lem10  27049  cvmlift3lem2  27057  nodenselem5  27673  nobndlem6  27685  outsidele  28010  mblfinlem1  28272  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  cnambfre  28284  itg2addnclem  28287  itg2addnclem3  28289  bddiblnc  28306  ftc1anclem7  28317  ftc1anc  28319  reftr  28405  comppfsc  28423  neibastop1  28424  neibastop2lem  28425  fdc  28485  sstotbnd2  28517  sstotbnd  28518  isbndx  28525  ssbnd  28531  totbndbnd  28532  heibor  28564  unichnidl  28675  elrfi  28875  fnwe2lem2  29249  hbtlem5  29329  pexmidlem8N  33194
  Copyright terms: Public domain W3C validator