Theorem rexlimdva 2607

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  ∃wrex 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  rexlimdvaa  2608  rexlimivv  2613  rexlimdvv  2614  ralxfrd  4480  rexxfrd  4481  fvelimab  5593  foco2  5775  elunirn  5788  f1elima  5795  mpoexw  6238  tfrlem5  6339  tfrlemibacc  6351  tfrlemibfn  6353  tfr1onlembacc  6367  tfr1onlembfn  6369  tfrcllembacc  6380  tfrcllembfn  6382  frecabcl  6424  nnaordex  6553  nnawordex  6554  ectocld  6627  phpm  6893  dif1enen  6908  fin0  6913  fin0or  6914  fimax2gtri  6929  fidcenum  6985  suplub2ti  7030  supisoex  7038  enomnilem  7166  finomni  7168  enmkvlem  7189  exmidfodomrlemeldju  7228  exmidfodomrlemreseldju  7229  ltexnqq  7437  ltbtwnnqq  7444  prarloclem4  7527  prarloc2  7533  genprndl  7550  genprndu  7551  prmuloc2  7596  1idprl  7619  1idpru  7620  cauappcvgprlemdisj  7680  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  caucvgprlemladdrl  7707  recexgt0sr  7802  map2psrprg  7834  suplocsrlem  7837  nntopi  7923  cnegexlem1  8162  cnegexlem2  8163  renegcl  8248  aptap  8637  supinfneg  9625  infsupneg  9626  qmulz  9653  elpq  9678  icc0r  9956  exbtwnzlemstep  10278  rebtwn2zlemstep  10283  ioo0  10290  ico0  10292  ioc0  10293  modqmuladd  10397  addmodlteq  10429  frec2uzrand  10436  frecuzrdgtcl  10443  frecuzrdgfunlem  10450  hashunlem  10816  shftlem  10857  caucvgre  11022  resqrexlemgt0  11061  rexico  11262  negfi  11268  climuni  11333  climshftlemg  11342  climcn1  11348  serf0  11392  summodclem2  11422  zsumdc  11424  fsum2dlemstep  11474  mertenslem2  11576  ntrivcvgap  11588  zproddc  11619  fprod2dlemstep  11662  dvds1lem  11841  odd2np1lem  11909  odd2np1  11910  sqoddm1div8z  11923  ltoddhalfle  11930  halfleoddlt  11931  m1expo  11937  divalglemeunn  11958  divalglemex  11959  divalglemeuneg  11960  flodddiv4  11971  bezoutlemaz  12036  bezoutlembz  12037  dvdssqim  12057  ncoprmgcdne1b  12121  coprmdvds2  12125  divgcdcoprm0  12133  cncongr1  12135  cncongr2  12136  dvdsnprmd  12157  rpexp  12185  pythagtriplem1  12297  pc2dvds  12362  difsqpwdvds  12370  oddprmdvds  12386  prmpwdvds  12387  4sqlem11  12433  dfgrp3mlem  13042  imasgrp2  13052  issubg4m  13132  imasabl  13273  ringinvnzdiv  13402  imasring  13414  dvdsrcl2  13449  dvdsrmul1  13452  lss1d  13699  lssats2  13730  lspsn  13732  dvdsrzring  13902  tgcl  14024  innei  14123  cnptoprest  14199  lmss  14206  lmtopcnp  14210  txlm  14239  blssps  14387  blss  14388  blssexps  14389  blssex  14390  mopni3  14444  metrest  14466  metcnp3  14471  mulc1cncf  14536  cncfco  14538  2lgsoddprmlem2  14915  subctctexmid  15212