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

Theorem rexlimdvaa 3154
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 458 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3153 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  rexlimddv  3159  tz7.7  6344  isofrlem  7286  nnawordex  8585  oaabs2  8596  fiin  9359  marypha1lem  9370  wemaplem3  9485  cantnflt  9609  fseqenlem2  9962  cardaleph  10026  coftr  10210  fin23lem26  10262  fin1a2lem13  10349  fpwwe2  10580  r1wunlim  10674  wunex2  10675  inttsk  10711  grur1  10757  inaprc  10773  receu  11801  zsupss  12863  xralrple  13125  rexanuz  15231  limsupval2  15363  caucvgb  15565  fsumiun  15707  rpnnen2lem12  16108  dvdsval2  16140  prmind2  16562  prmdvdsncoprmbd  16603  pcprmpw2  16755  pockthg  16779  prmreclem5  16793  vdwlem6  16859  vdwlem10  16863  sscpwex  17699  drsdirfi  18195  psgnunilem3  19279  sylow3lem2  19411  efgsfo  19522  lt6abl  19673  ghmcyg  19674  ablsimpgfind  19890  unitgrp  20097  irredrmul  20137  drngnidl  20702  znunit  20973  tgcl  22322  neiint  22458  restopnb  22529  ordtrest2lem  22557  pnfnei  22574  mnfnei  22575  iscnp4  22617  haust1  22706  ordthauslem  22737  tgcmp  22755  t1connperf  22790  2ndc1stc  22805  2ndcdisj  22810  islly2  22838  nllyrest  22840  reftr  22868  comppfsc  22886  ptbasfi  22935  ptcnp  22976  xkococnlem  23013  tgqtop  23066  fbssfi  23191  fgabs  23233  neifil  23234  trfil2  23241  elfm2  23302  elfm3  23304  rnelfmlem  23306  fmfnfmlem4  23311  flffbas  23349  fclsfnflim  23381  ptcmplem4  23409  tsmsxp  23509  blssexps  23782  blssex  23783  icccmplem3  24190  cnheibor  24321  pi1blem  24405  iscfil3  24640  iscmet3lem2  24659  metsscmetcld  24682  ovolicc2  24889  nulmbl2  24903  volsup  24923  dyadmbllem  24966  itg2const2  25109  bddmulibl  25206  bddiblnc  25209  limcflf  25248  itgsubst  25416  ulmdvlem3  25764  xrlimcnp  26321  amgm  26343  dchrptlem2  26616  lgsne0  26686  lgsqr  26702  lgsquadlem1  26731  dchrvmasumif  26854  rpvmasum2  26863  dchrisum0re  26864  dchrisum0lem3  26870  dchrisum0  26871  dchrmusum  26875  dchrvmasum  26876  chpdifbnd  26906  pntrlog2bnd  26935  pntibndlem3  26943  pntibnd  26944  pntleml  26962  ostth  26990  nosupno  27054  nosupbnd1lem1  27059  nosupbnd2  27067  noinfno  27069  noinfbnd1lem1  27074  noinfbnd2  27082  scutbdaybnd2  27158  oldlim  27219  oldbdayim  27221  sleadd1  27301  brbtwn2  27857  colinearalg  27862  nbumgrvtx  28297  cusgrfilem1  28406  nmobndi  29720  spansneleq  30515  ofrn2  31559  xreceu  31781  ordtrest2NEWlem  32506  dya2iocnei  32885  connpconn  33832  cvmsss2  33871  cvmlift2lem10  33909  cvmlift3lem2  33917  outsidele  34720  neibastop1  34834  neibastop2lem  34835  matunitlindflem1  36077  mblfinlem1  36118  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  cnambfre  36129  itg2addnclem  36132  itg2addnclem3  36134  ftc1anclem7  36160  ftc1anc  36162  fdc  36207  sstotbnd2  36236  sstotbnd  36237  isbndx  36244  ssbnd  36250  totbndbnd  36251  heibor  36283  unichnidl  36493  pexmidlem8N  38443  sn-0tie0  40911  nna4b4nsq  41001  elrfi  41020  fnwe2lem2  41381  hbtlem5  41458  rexlimdvaacbv  42485  rexlimddvcbvw  42486  liminfval2  44016  2zrngamgm  46244
  Copyright terms: Public domain W3C validator