Theorem rexlimdva 2552

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 114	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 2551	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  ∃wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  rexlimdvaa  2553  rexlimivv  2558  rexlimdvv  2559  ralxfrd  4391  rexxfrd  4392  fvelimab  5485  foco2  5663  elunirn  5675  f1elima  5682  tfrlem5  6219  tfrlemibacc  6231  tfrlemibfn  6233  tfr1onlembacc  6247  tfr1onlembfn  6249  tfrcllembacc  6260  tfrcllembfn  6262  frecabcl  6304  nnaordex  6431  nnawordex  6432  ectocld  6503  phpm  6767  dif1enen  6782  fin0  6787  fin0or  6788  fimax2gtri  6803  fidcenum  6852  suplub2ti  6896  supisoex  6904  enomnilem  7018  finomni  7020  enmkvlem  7043  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  ltexnqq  7240  ltbtwnnqq  7247  prarloclem4  7330  prarloc2  7336  genprndl  7353  genprndu  7354  prmuloc2  7399  1idprl  7422  1idpru  7423  cauappcvgprlemdisj  7483  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  recexgt0sr  7605  map2psrprg  7637  suplocsrlem  7640  nntopi  7726  cnegexlem1  7961  cnegexlem2  7962  renegcl  8047  supinfneg  9417  infsupneg  9418  qmulz  9442  elpq  9467  icc0r  9739  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  ioo0  10068  ico0  10070  ioc0  10071  modqmuladd  10170  addmodlteq  10202  frec2uzrand  10209  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  hashunlem  10582  shftlem  10620  caucvgre  10785  resqrexlemgt0  10824  rexico  11025  negfi  11031  climuni  11094  climshftlemg  11103  climcn1  11109  serf0  11153  summodclem2  11183  zsumdc  11185  fsum2dlemstep  11235  mertenslem2  11337  ntrivcvgap  11349  zproddc  11380  dvds1lem  11540  odd2np1lem  11605  odd2np1  11606  sqoddm1div8z  11619  ltoddhalfle  11626  halfleoddlt  11627  m1expo  11633  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  flodddiv4  11667  bezoutlemaz  11727  bezoutlembz  11728  dvdssqim  11748  ncoprmgcdne1b  11806  coprmdvds2  11810  divgcdcoprm0  11818  cncongr1  11820  cncongr2  11821  dvdsnprmd  11842  rpexp  11867  tgcl  12272  innei  12371  cnptoprest  12447  lmss  12454  lmtopcnp  12458  txlm  12487  blssps  12635  blss  12636  blssexps  12637  blssex  12638  mopni3  12692  metrest  12714  metcnp3  12719  mulc1cncf  12784  cncfco  12786  subctctexmid  13369