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

Theorem rexlimdvaa 3014
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 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimdvaa (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvaa
StepHypRef Expression
1 rexlimdvaa.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
21expr 641 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3013 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  rexlimddv  3017  tz7.7  5666  isofrlem  6490  nnawordex  7604  oaabs2  7612  fiin  8211  marypha1lem  8222  wemaplem3  8336  cantnflt  8452  fseqenlem2  8731  cardaleph  8795  coftr  8978  fin23lem26  9030  fin1a2lem13  9117  fpwwe2  9344  r1wunlim  9438  wunex2  9439  inttsk  9475  grur1  9521  inaprc  9537  receu  10551  zsupss  11653  xralrple  11910  rexanuz  13933  limsupval2  14059  caucvgb  14258  fsumiun  14394  rpnnen2lem12  14793  dvdsval2  14824  prmind2  15236  pcprmpw2  15424  pockthg  15448  prmreclem5  15462  vdwlem6  15528  vdwlem10  15532  sscpwex  16298  drsdirfi  16761  psgnunilem3  17739  sylow3lem2  17866  efgsfo  17975  lt6abl  18119  ghmcyg  18120  unitgrp  18490  irredrmul  18530  drngnidl  19050  znunit  19731  tgcl  20584  neiint  20718  restopnb  20789  ordtrest2lem  20817  pnfnei  20834  mnfnei  20835  iscnp4  20877  haust1  20966  ordthauslem  20997  tgcmp  21014  t1conperf  21049  2ndc1stc  21064  2ndcdisj  21069  islly2  21097  nllyrest  21099  reftr  21127  comppfsc  21145  ptbasfi  21194  ptcnp  21235  xkococnlem  21272  tgqtop  21325  fbssfi  21451  fgabs  21493  neifil  21494  trfil2  21501  elfm2  21562  elfm3  21564  rnelfmlem  21566  fmfnfmlem4  21571  flffbas  21609  fclsfnflim  21641  ptcmplem4  21669  tsmsxp  21768  blssexps  22041  blssex  22042  icccmplem3  22435  cnheibor  22562  pi1blem  22647  iscfil3  22879  iscmet3lem2  22898  cmetss  22921  ovolicc2  23097  nulmbl2  23111  volsup  23131  dyadmbllem  23173  itg2const2  23314  bddmulibl  23411  limcflf  23451  itgsubst  23616  ulmdvlem3  23960  xrlimcnp  24495  amgm  24517  dchrptlem2  24790  lgsne0  24860  lgsqr  24876  lgsquadlem1  24905  dchrvmasumif  24992  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  dchrmusum  25013  dchrvmasum  25014  chpdifbnd  25044  pntrlog2bnd  25073  pntibndlem3  25081  pntibnd  25082  pntleml  25100  ostth  25128  brbtwn2  25585  colinearalg  25590  cusgrafilem1  26007  nmobndi  27014  spansneleq  27813  ofrn2  28822  xreceu  28961  ordtrest2NEWlem  29296  dya2iocnei  29671  conpcon  30471  cvmsss2  30510  cvmlift2lem10  30548  cvmlift3lem2  30556  nodenselem5  31084  nobndlem6  31096  outsidele  31409  neibastop1  31524  neibastop2lem  31525  matunitlindflem1  32575  mblfinlem1  32616  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  cnambfre  32628  itg2addnclem  32631  itg2addnclem3  32633  bddiblnc  32650  ftc1anclem7  32661  ftc1anc  32663  fdc  32711  sstotbnd2  32743  sstotbnd  32744  isbndx  32751  ssbnd  32757  totbndbnd  32758  heibor  32790  unichnidl  33000  pexmidlem8N  34281  elrfi  36275  fnwe2lem2  36639  hbtlem5  36717  nbumgrvtx  40568  cusgrfilem1  40671  2zrngamgm  41729
  Copyright terms: Public domain W3C validator