Theorem rexlimdva 2502

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 2501	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1445  ∃wrex 2371

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-i5r 1480

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375  df-rex 2376

This theorem is referenced by:  rexlimdvaa  2503  rexlimivv  2508  rexlimdvv  2509  ralxfrd  4312  rexxfrd  4313  fvelimab  5395  foco2  5571  elunirn  5583  f1elima  5590  tfrlem5  6117  tfrlemibacc  6129  tfrlemibfn  6131  tfr1onlembacc  6145  tfr1onlembfn  6147  tfrcllembacc  6158  tfrcllembfn  6160  frecabcl  6202  nnaordex  6326  nnawordex  6327  ectocld  6398  phpm  6661  dif1enen  6676  fin0  6681  fin0or  6682  fimax2gtri  6697  fidcenum  6745  suplub2ti  6776  supisoex  6784  enomnilem  6881  finomni  6883  exmidfodomrlemeldju  6922  exmidfodomrlemreseldju  6923  ltexnqq  7064  ltbtwnnqq  7071  prarloclem4  7154  prarloc2  7160  genprndl  7177  genprndu  7178  prmuloc2  7223  1idprl  7246  1idpru  7247  cauappcvgprlemdisj  7307  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  caucvgprlemladdrl  7334  recexgt0sr  7416  nntopi  7526  cnegexlem1  7754  cnegexlem2  7755  renegcl  7840  supinfneg  9182  infsupneg  9183  qmulz  9207  icc0r  9492  exbtwnzlemstep  9808  rebtwn2zlemstep  9813  ioo0  9820  ico0  9822  ioc0  9823  modqmuladd  9922  addmodlteq  9954  frec2uzrand  9961  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  hashunlem  10343  shftlem  10381  caucvgre  10545  resqrexlemgt0  10584  rexico  10785  negfi  10790  climuni  10852  climshftlemg  10861  climcn1  10867  serf0  10911  summodclem2  10941  zsumdc  10943  fsum2dlemstep  10993  mertenslem2  11095  dvds1lem  11250  odd2np1lem  11315  odd2np1  11316  sqoddm1div8z  11329  ltoddhalfle  11336  halfleoddlt  11337  m1expo  11343  divalglemeunn  11364  divalglemex  11365  divalglemeuneg  11366  flodddiv4  11377  bezoutlemaz  11435  bezoutlembz  11436  dvdssqim  11456  ncoprmgcdne1b  11514  coprmdvds2  11518  divgcdcoprm0  11526  cncongr1  11528  cncongr2  11529  dvdsnprmd  11550  rpexp  11575  tgcl  11932  innei  12031  cnptoprest  12106  lmss  12113  lmtopcnp  12117  blssps  12229  blss  12230  blssexps  12231  blssex  12232  mopni3  12286  metrest  12308  metcnp3  12309  mulc1cncf  12358  cncfco  12360