Theorem rexlimdva 2485

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 113	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 2484	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1436  ∃wrex 2356

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-i5r 1471

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-ral 2360  df-rex 2361

This theorem is referenced by:  rexlimdvaa  2486  rexlimivv  2490  rexlimdvv  2491  ralxfrd  4251  rexxfrd  4252  fvelimab  5308  foco2  5476  elunirn  5488  f1elima  5495  tfrlem5  6014  tfrlemibacc  6026  tfrlemibfn  6028  tfr1onlembacc  6042  tfr1onlembfn  6044  tfrcllembacc  6055  tfrcllembfn  6057  frecabcl  6099  nnaordex  6219  nnawordex  6220  ectocld  6291  phpm  6514  dif1enen  6529  fin0  6534  fin0or  6535  suplub2ti  6617  supisoex  6625  enomnilem  6715  finomni  6717  exmidfodomrlemeldju  6746  exmidfodomrlemreseldju  6747  ltexnqq  6888  ltbtwnnqq  6895  prarloclem4  6978  prarloc2  6984  genprndl  7001  genprndu  7002  prmuloc2  7047  1idprl  7070  1idpru  7071  cauappcvgprlemdisj  7131  cauappcvgprlemladdru  7136  cauappcvgprlemladdrl  7137  caucvgprlemladdrl  7158  recexgt0sr  7240  nntopi  7350  cnegexlem1  7578  cnegexlem2  7579  renegcl  7664  supinfneg  8992  infsupneg  8993  qmulz  9017  icc0r  9253  exbtwnzlemstep  9562  rebtwn2zlemstep  9567  ioo0  9574  ico0  9576  ioc0  9577  modqmuladd  9676  addmodlteq  9708  frec2uzrand  9715  frecuzrdgtcl  9722  frecuzrdgfunlem  9729  hashunlem  10061  shftlem  10092  caucvgre  10255  resqrexlemgt0  10294  rexico  10495  negfi  10498  climuni  10520  climshftlemg  10529  climcn1  10535  serif0  10577  dvds1lem  10601  odd2np1lem  10666  odd2np1  10667  sqoddm1div8z  10680  ltoddhalfle  10687  halfleoddlt  10688  m1expo  10694  divalglemeunn  10715  divalglemex  10716  divalglemeuneg  10717  flodddiv4  10728  bezoutlemaz  10786  bezoutlembz  10787  dvdssqim  10807  ncoprmgcdne1b  10865  coprmdvds2  10869  divgcdcoprm0  10877  cncongr1  10879  cncongr2  10880  dvdsnprmd  10901  rpexp  10926