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

Theorem rexlimdvaa 3026
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 642 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3025 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2912  df-rex 2913
This theorem is referenced by:  rexlimddv  3029  tz7.7  5713  isofrlem  6550  nnawordex  7669  oaabs2  7677  fiin  8280  marypha1lem  8291  wemaplem3  8405  cantnflt  8521  fseqenlem2  8800  cardaleph  8864  coftr  9047  fin23lem26  9099  fin1a2lem13  9186  fpwwe2  9417  r1wunlim  9511  wunex2  9512  inttsk  9548  grur1  9594  inaprc  9610  receu  10624  zsupss  11729  xralrple  11987  rexanuz  14027  limsupval2  14153  caucvgb  14352  fsumiun  14491  rpnnen2lem12  14890  dvdsval2  14921  prmind2  15333  pcprmpw2  15521  pockthg  15545  prmreclem5  15559  vdwlem6  15625  vdwlem10  15629  sscpwex  16407  drsdirfi  16870  psgnunilem3  17848  sylow3lem2  17975  efgsfo  18084  lt6abl  18228  ghmcyg  18229  unitgrp  18599  irredrmul  18639  drngnidl  19161  znunit  19844  tgcl  20697  neiint  20831  restopnb  20902  ordtrest2lem  20930  pnfnei  20947  mnfnei  20948  iscnp4  20990  haust1  21079  ordthauslem  21110  tgcmp  21127  t1connperf  21162  2ndc1stc  21177  2ndcdisj  21182  islly2  21210  nllyrest  21212  reftr  21240  comppfsc  21258  ptbasfi  21307  ptcnp  21348  xkococnlem  21385  tgqtop  21438  fbssfi  21564  fgabs  21606  neifil  21607  trfil2  21614  elfm2  21675  elfm3  21677  rnelfmlem  21679  fmfnfmlem4  21684  flffbas  21722  fclsfnflim  21754  ptcmplem4  21782  tsmsxp  21881  blssexps  22154  blssex  22155  icccmplem3  22550  cnheibor  22677  pi1blem  22762  iscfil3  22994  iscmet3lem2  23013  cmetss  23036  ovolicc2  23213  nulmbl2  23227  volsup  23247  dyadmbllem  23290  itg2const2  23431  bddmulibl  23528  limcflf  23568  itgsubst  23733  ulmdvlem3  24077  xrlimcnp  24612  amgm  24634  dchrptlem2  24907  lgsne0  24977  lgsqr  24993  lgsquadlem1  25022  dchrvmasumif  25109  rpvmasum2  25118  dchrisum0re  25119  dchrisum0lem3  25125  dchrisum0  25126  dchrmusum  25130  dchrvmasum  25131  chpdifbnd  25161  pntrlog2bnd  25190  pntibndlem3  25198  pntibnd  25199  pntleml  25217  ostth  25245  brbtwn2  25702  colinearalg  25707  nbumgrvtx  26146  cusgrfilem1  26255  nmobndi  27500  spansneleq  28299  ofrn2  29307  xreceu  29439  ordtrest2NEWlem  29774  dya2iocnei  30149  connpconn  30960  cvmsss2  30999  cvmlift2lem10  31037  cvmlift3lem2  31045  nodenselem5  31583  nobndlem6  31595  nosino  31610  outsidele  31916  neibastop1  32031  neibastop2lem  32032  matunitlindflem1  33072  mblfinlem1  33113  mblfinlem3  33115  mblfinlem4  33116  ismblfin  33117  cnambfre  33125  itg2addnclem  33128  itg2addnclem3  33130  bddiblnc  33147  ftc1anclem7  33158  ftc1anc  33160  fdc  33208  sstotbnd2  33240  sstotbnd  33241  isbndx  33248  ssbnd  33254  totbndbnd  33255  heibor  33287  unichnidl  33497  pexmidlem8N  34778  elrfi  36772  fnwe2lem2  37136  hbtlem5  37214  2zrngamgm  41253
  Copyright terms: Public domain W3C validator