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

Theorem rexlimdvaa 2948
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 2947 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   E.wrex 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2804  df-rex 2805
This theorem is referenced by:  rexlimddv  2951  tz7.7  4854  isofrlem  6141  nnawordex  7187  oaabs2  7195  fiin  7784  marypha1lem  7795  wemaplem3  7874  cantnflt  7992  cantnfltOLD  8022  fseqenlem2  8307  cardaleph  8371  coftr  8554  fin23lem26  8606  fin1a2lem13  8693  fpwwe2  8922  r1wunlim  9016  wunex2  9017  inttsk  9053  grur1  9099  inaprc  9115  receu  10093  zsupss  11056  xralrple  11287  rexanuz  12952  limsupval2  13077  caucvgb  13276  fsumiun  13403  rpnnen2  13627  dvdsval2  13657  prmind2  13893  pcprmpw2  14067  pockthg  14086  prmreclem5  14100  vdwlem6  14166  vdwlem10  14170  sscpwex  14848  drsdirfi  15228  psgnunilem3  16122  sylow3lem2  16249  efgsfo  16358  lt6abl  16493  ghmcyg  16494  unitgrp  16883  irredrmul  16923  drngnidl  17435  znunit  18122  tgcl  18707  neiint  18841  restopnb  18912  ordtrest2lem  18940  pnfnei  18957  mnfnei  18958  iscnp4  19000  haust1  19089  ordthauslem  19120  tgcmp  19137  t1conperf  19173  2ndc1stc  19188  2ndcdisj  19193  islly2  19221  nllyrest  19223  ptbasfi  19287  ptcnp  19328  xkococnlem  19365  tgqtop  19418  fbssfi  19543  fgabs  19585  neifil  19586  trfil2  19593  elfm2  19654  elfm3  19656  rnelfmlem  19658  fmfnfmlem4  19663  flffbas  19701  fclsfnflim  19733  ptcmplem4  19760  tsmsxp  19862  blssexps  20134  blssex  20135  icccmplem3  20534  cnheibor  20660  pi1blem  20744  iscfil3  20917  iscmet3lem2  20936  cmetss  20958  ovolicc2  21138  nulmbl2  21152  volsup  21171  dyadmbllem  21213  itg2const2  21353  bddmulibl  21450  limcflf  21490  itgsubst  21655  ulmdvlem3  22001  xrlimcnp  22496  amgm  22518  dchrptlem2  22738  lgsne0  22806  lgsqr  22819  lgsquadlem1  22827  dchrvmasumif  22886  rpvmasum2  22895  dchrisum0re  22896  dchrisum0lem3  22902  dchrisum0  22903  dchrmusum  22907  dchrvmasum  22908  chpdifbnd  22938  pntrlog2bnd  22967  pntibndlem3  22975  pntibnd  22976  pntleml  22994  ostth  23022  brbtwn2  23304  colinearalg  23309  cusgrafilem1  23540  nmobndi  24328  spansneleq  25126  ofrn2  26110  xreceu  26243  ordtrest2NEWlem  26498  dya2iocnei  26842  conpcon  27269  cvmsss2  27308  cvmlift2lem10  27346  cvmlift3lem2  27354  nodenselem5  27971  nobndlem6  27983  outsidele  28308  mblfinlem1  28577  mblfinlem3  28579  mblfinlem4  28580  ismblfin  28581  cnambfre  28589  itg2addnclem  28592  itg2addnclem3  28594  bddiblnc  28611  ftc1anclem7  28622  ftc1anc  28624  reftr  28710  comppfsc  28728  neibastop1  28729  neibastop2lem  28730  fdc  28790  sstotbnd2  28822  sstotbnd  28823  isbndx  28830  ssbnd  28836  totbndbnd  28837  heibor  28869  unichnidl  28980  elrfi  29179  fnwe2lem2  29553  hbtlem5  29633  pexmidlem8N  33960
  Copyright terms: Public domain W3C validator