Theorem rexlimdva 2587

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∃wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  rexlimdvaa  2588  rexlimivv  2593  rexlimdvv  2594  ralxfrd  4445  rexxfrd  4446  fvelimab  5550  foco2  5731  elunirn  5743  f1elima  5750  mpoexw  6190  tfrlem5  6291  tfrlemibacc  6303  tfrlemibfn  6305  tfr1onlembacc  6319  tfr1onlembfn  6321  tfrcllembacc  6332  tfrcllembfn  6334  frecabcl  6376  nnaordex  6504  nnawordex  6505  ectocld  6576  phpm  6840  dif1enen  6855  fin0  6860  fin0or  6861  fimax2gtri  6876  fidcenum  6930  suplub2ti  6975  supisoex  6983  enomnilem  7111  finomni  7113  enmkvlem  7134  exmidfodomrlemeldju  7165  exmidfodomrlemreseldju  7166  ltexnqq  7359  ltbtwnnqq  7366  prarloclem4  7449  prarloc2  7455  genprndl  7472  genprndu  7473  prmuloc2  7518  1idprl  7541  1idpru  7542  cauappcvgprlemdisj  7602  cauappcvgprlemladdru  7607  cauappcvgprlemladdrl  7608  caucvgprlemladdrl  7629  recexgt0sr  7724  map2psrprg  7756  suplocsrlem  7759  nntopi  7845  cnegexlem1  8083  cnegexlem2  8084  renegcl  8169  supinfneg  9543  infsupneg  9544  qmulz  9571  elpq  9596  icc0r  9872  exbtwnzlemstep  10193  rebtwn2zlemstep  10198  ioo0  10205  ico0  10207  ioc0  10208  modqmuladd  10311  addmodlteq  10343  frec2uzrand  10350  frecuzrdgtcl  10357  frecuzrdgfunlem  10364  hashunlem  10728  shftlem  10769  caucvgre  10934  resqrexlemgt0  10973  rexico  11174  negfi  11180  climuni  11245  climshftlemg  11254  climcn1  11260  serf0  11304  summodclem2  11334  zsumdc  11336  fsum2dlemstep  11386  mertenslem2  11488  ntrivcvgap  11500  zproddc  11531  fprod2dlemstep  11574  dvds1lem  11753  odd2np1lem  11820  odd2np1  11821  sqoddm1div8z  11834  ltoddhalfle  11841  halfleoddlt  11842  m1expo  11848  divalglemeunn  11869  divalglemex  11870  divalglemeuneg  11871  flodddiv4  11882  bezoutlemaz  11947  bezoutlembz  11948  dvdssqim  11968  ncoprmgcdne1b  12032  coprmdvds2  12036  divgcdcoprm0  12044  cncongr1  12046  cncongr2  12047  dvdsnprmd  12068  rpexp  12096  pythagtriplem1  12208  pc2dvds  12272  difsqpwdvds  12280  oddprmdvds  12295  prmpwdvds  12296  tgcl  12819  innei  12918  cnptoprest  12994  lmss  13001  lmtopcnp  13005  txlm  13034  blssps  13182  blss  13183  blssexps  13184  blssex  13185  mopni3  13239  metrest  13261  metcnp3  13266  mulc1cncf  13331  cncfco  13333  subctctexmid  13996