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

Theorem rexlimdvaa 3180
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 444 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3179 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  rexlimddv  3183  tz7.7  5891  isofrlem  6735  nnawordex  7874  oaabs2  7882  fiin  8487  marypha1lem  8498  wemaplem3  8612  cantnflt  8736  fseqenlem2  9051  cardaleph  9115  coftr  9300  fin23lem26  9352  fin1a2lem13  9439  fpwwe2  9670  r1wunlim  9764  wunex2  9765  inttsk  9801  grur1  9847  inaprc  9863  receu  10877  zsupss  11984  xralrple  12240  rexanuz  14292  limsupval2  14418  caucvgb  14617  fsumiun  14759  rpnnen2lem12  15159  dvdsval2  15191  prmind2  15604  pcprmpw2  15792  pockthg  15816  prmreclem5  15830  vdwlem6  15896  vdwlem10  15900  sscpwex  16681  drsdirfi  17145  psgnunilem3  18122  sylow3lem2  18249  efgsfo  18358  lt6abl  18502  ghmcyg  18503  unitgrp  18874  irredrmul  18914  drngnidl  19443  znunit  20126  tgcl  20993  neiint  21128  restopnb  21199  ordtrest2lem  21227  pnfnei  21244  mnfnei  21245  iscnp4  21287  haust1  21376  ordthauslem  21407  tgcmp  21424  t1connperf  21459  2ndc1stc  21474  2ndcdisj  21479  islly2  21507  nllyrest  21509  reftr  21537  comppfsc  21555  ptbasfi  21604  ptcnp  21645  xkococnlem  21682  tgqtop  21735  fbssfi  21860  fgabs  21902  neifil  21903  trfil2  21910  elfm2  21971  elfm3  21973  rnelfmlem  21975  fmfnfmlem4  21980  flffbas  22018  fclsfnflim  22050  ptcmplem4  22078  tsmsxp  22177  blssexps  22450  blssex  22451  icccmplem3  22846  cnheibor  22973  pi1blem  23057  iscfil3  23289  iscmet3lem2  23308  cmetss  23331  ovolicc2  23509  nulmbl2  23523  volsup  23543  dyadmbllem  23586  itg2const2  23727  bddmulibl  23824  limcflf  23864  itgsubst  24031  ulmdvlem3  24375  xrlimcnp  24915  amgm  24937  dchrptlem2  25210  lgsne0  25280  lgsqr  25296  lgsquadlem1  25325  dchrvmasumif  25412  rpvmasum2  25421  dchrisum0re  25422  dchrisum0lem3  25428  dchrisum0  25429  dchrmusum  25433  dchrvmasum  25434  chpdifbnd  25464  pntrlog2bnd  25493  pntibndlem3  25501  pntibnd  25502  pntleml  25520  ostth  25548  brbtwn2  26005  colinearalg  26010  nbumgrvtx  26464  cusgrfilem1  26585  nmobndi  27969  spansneleq  28768  ofrn2  29781  xreceu  29969  ordtrest2NEWlem  30307  dya2iocnei  30683  connpconn  31554  cvmsss2  31593  cvmlift2lem10  31631  cvmlift3lem2  31639  nosupno  32185  nosupbnd1lem1  32190  nosupbnd2  32198  scutbdaybnd  32257  outsidele  32575  neibastop1  32690  neibastop2lem  32691  matunitlindflem1  33737  mblfinlem1  33778  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  cnambfre  33789  itg2addnclem  33792  itg2addnclem3  33794  bddiblnc  33811  ftc1anclem7  33822  ftc1anc  33824  fdc  33872  sstotbnd2  33904  sstotbnd  33905  isbndx  33912  ssbnd  33918  totbndbnd  33919  heibor  33951  unichnidl  34161  pexmidlem8N  35785  elrfi  37783  fnwe2lem2  38147  hbtlem5  38224  liminfval2  40515  2zrngamgm  42464
  Copyright terms: Public domain W3C validator