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

Theorem rexlimdvaa 3231
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 446 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3230 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  wrex 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3112  df-rex 3113
This theorem is referenced by:  rexlimddv  3234  tz7.7  5973  isofrlem  6821  nnawordex  7961  oaabs2  7969  fiin  8574  marypha1lem  8585  wemaplem3  8699  cantnflt  8823  fseqenlem2  9138  cardaleph  9202  coftr  9387  fin23lem26  9439  fin1a2lem13  9526  fpwwe2  9757  r1wunlim  9851  wunex2  9852  inttsk  9888  grur1  9934  inaprc  9950  receu  10964  zsupss  12003  xralrple  12261  rexanuz  14315  limsupval2  14441  caucvgb  14640  fsumiun  14782  rpnnen2lem12  15181  dvdsval2  15213  prmind2  15623  pcprmpw2  15810  pockthg  15834  prmreclem5  15848  vdwlem6  15914  vdwlem10  15918  sscpwex  16686  drsdirfi  17150  psgnunilem3  18124  sylow3lem2  18251  efgsfo  18360  lt6abl  18504  ghmcyg  18505  unitgrp  18876  irredrmul  18916  drngnidl  19445  znunit  20126  tgcl  20995  neiint  21130  restopnb  21201  ordtrest2lem  21229  pnfnei  21246  mnfnei  21247  iscnp4  21289  haust1  21378  ordthauslem  21409  tgcmp  21426  t1connperf  21461  2ndc1stc  21476  2ndcdisj  21481  islly2  21509  nllyrest  21511  reftr  21539  comppfsc  21557  ptbasfi  21606  ptcnp  21647  xkococnlem  21684  tgqtop  21737  fbssfi  21862  fgabs  21904  neifil  21905  trfil2  21912  elfm2  21973  elfm3  21975  rnelfmlem  21977  fmfnfmlem4  21982  flffbas  22020  fclsfnflim  22052  ptcmplem4  22080  tsmsxp  22179  blssexps  22452  blssex  22453  icccmplem3  22848  cnheibor  22975  pi1blem  23059  iscfil3  23292  iscmet3lem2  23311  cmetss  23334  ovolicc2  23513  nulmbl2  23527  volsup  23547  dyadmbllem  23590  itg2const2  23732  bddmulibl  23829  limcflf  23869  itgsubst  24036  ulmdvlem3  24380  xrlimcnp  24919  amgm  24941  dchrptlem2  25214  lgsne0  25284  lgsqr  25300  lgsquadlem1  25329  dchrvmasumif  25416  rpvmasum2  25425  dchrisum0re  25426  dchrisum0lem3  25432  dchrisum0  25433  dchrmusum  25437  dchrvmasum  25438  chpdifbnd  25468  pntrlog2bnd  25497  pntibndlem3  25505  pntibnd  25506  pntleml  25524  ostth  25552  brbtwn2  26009  colinearalg  26014  nbumgrvtx  26468  cusgrfilem1  26589  nmobndi  27968  spansneleq  28767  ofrn2  29779  xreceu  29965  ordtrest2NEWlem  30303  dya2iocnei  30679  connpconn  31549  cvmsss2  31588  cvmlift2lem10  31626  cvmlift3lem2  31634  nosupno  32179  nosupbnd1lem1  32184  nosupbnd2  32192  scutbdaybnd  32251  outsidele  32569  neibastop1  32684  neibastop2lem  32685  matunitlindflem1  33724  mblfinlem1  33765  mblfinlem3  33767  mblfinlem4  33768  ismblfin  33769  cnambfre  33776  itg2addnclem  33779  itg2addnclem3  33781  bddiblnc  33798  ftc1anclem7  33809  ftc1anc  33811  fdc  33858  sstotbnd2  33890  sstotbnd  33891  isbndx  33898  ssbnd  33904  totbndbnd  33905  heibor  33937  unichnidl  34147  pexmidlem8N  35763  elrfi  37764  fnwe2lem2  38127  hbtlem5  38204  liminfval2  40485  2zrngamgm  42512
  Copyright terms: Public domain W3C validator