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

Theorem rexlimdvaa 3170
 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 644 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 3169 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139  ∃wrex 3051 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056 This theorem is referenced by:  rexlimddv  3173  tz7.7  5910  isofrlem  6753  nnawordex  7886  oaabs2  7894  fiin  8493  marypha1lem  8504  wemaplem3  8618  cantnflt  8742  fseqenlem2  9038  cardaleph  9102  coftr  9287  fin23lem26  9339  fin1a2lem13  9426  fpwwe2  9657  r1wunlim  9751  wunex2  9752  inttsk  9788  grur1  9834  inaprc  9850  receu  10864  zsupss  11970  xralrple  12229  rexanuz  14284  limsupval2  14410  caucvgb  14609  fsumiun  14752  rpnnen2lem12  15153  dvdsval2  15185  prmind2  15600  pcprmpw2  15788  pockthg  15812  prmreclem5  15826  vdwlem6  15892  vdwlem10  15896  sscpwex  16676  drsdirfi  17139  psgnunilem3  18116  sylow3lem2  18243  efgsfo  18352  lt6abl  18496  ghmcyg  18497  unitgrp  18867  irredrmul  18907  drngnidl  19431  znunit  20114  tgcl  20975  neiint  21110  restopnb  21181  ordtrest2lem  21209  pnfnei  21226  mnfnei  21227  iscnp4  21269  haust1  21358  ordthauslem  21389  tgcmp  21406  t1connperf  21441  2ndc1stc  21456  2ndcdisj  21461  islly2  21489  nllyrest  21491  reftr  21519  comppfsc  21537  ptbasfi  21586  ptcnp  21627  xkococnlem  21664  tgqtop  21717  fbssfi  21842  fgabs  21884  neifil  21885  trfil2  21892  elfm2  21953  elfm3  21955  rnelfmlem  21957  fmfnfmlem4  21962  flffbas  22000  fclsfnflim  22032  ptcmplem4  22060  tsmsxp  22159  blssexps  22432  blssex  22433  icccmplem3  22828  cnheibor  22955  pi1blem  23039  iscfil3  23271  iscmet3lem2  23290  cmetss  23313  ovolicc2  23490  nulmbl2  23504  volsup  23524  dyadmbllem  23567  itg2const2  23707  bddmulibl  23804  limcflf  23844  itgsubst  24011  ulmdvlem3  24355  xrlimcnp  24894  amgm  24916  dchrptlem2  25189  lgsne0  25259  lgsqr  25275  lgsquadlem1  25304  dchrvmasumif  25391  rpvmasum2  25400  dchrisum0re  25401  dchrisum0lem3  25407  dchrisum0  25408  dchrmusum  25412  dchrvmasum  25413  chpdifbnd  25443  pntrlog2bnd  25472  pntibndlem3  25480  pntibnd  25481  pntleml  25499  ostth  25527  brbtwn2  25984  colinearalg  25989  nbumgrvtx  26441  cusgrfilem1  26561  nmobndi  27939  spansneleq  28738  ofrn2  29751  xreceu  29939  ordtrest2NEWlem  30277  dya2iocnei  30653  connpconn  31524  cvmsss2  31563  cvmlift2lem10  31601  cvmlift3lem2  31609  nosupno  32155  nosupbnd1lem1  32160  nosupbnd2  32168  scutbdaybnd  32227  outsidele  32545  neibastop1  32660  neibastop2lem  32661  matunitlindflem1  33718  mblfinlem1  33759  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  cnambfre  33771  itg2addnclem  33774  itg2addnclem3  33776  bddiblnc  33793  ftc1anclem7  33804  ftc1anc  33806  fdc  33854  sstotbnd2  33886  sstotbnd  33887  isbndx  33894  ssbnd  33900  totbndbnd  33901  heibor  33933  unichnidl  34143  pexmidlem8N  35766  elrfi  37759  fnwe2lem2  38123  hbtlem5  38200  liminfval2  40503  2zrngamgm  42449
 Copyright terms: Public domain W3C validator