Theorem rexlimdva 2668

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  rexlimdvaa  2669  rexlimivv  2674  rexlimdvv  2675  ralxfrd  4610  rexxfrd  4611  fvelimab  5762  foco2  5962  elunirn  5975  f1elima  5982  mpoexw  6453  tfrlem5  6589  tfrlemibacc  6601  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembfn  6632  frecabcl  6674  nnaordex  6805  nnawordex  6806  ectocld  6879  phpm  7172  dif1enen  7189  fin0  7194  fin0or  7195  fimax2gtri  7211  fidcenum  7279  suplub2ti  7348  supisoex  7356  enomnilem  7485  finomni  7487  enmkvlem  7508  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  ltexnqq  7782  ltbtwnnqq  7789  prarloclem4  7872  prarloc2  7878  genprndl  7895  genprndu  7896  prmuloc2  7941  1idprl  7964  1idpru  7965  cauappcvgprlemdisj  8025  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  recexgt0sr  8147  map2psrprg  8179  suplocsrlem  8182  nntopi  8268  cnegexlem1  8509  cnegexlem2  8510  renegcl  8595  aptap  8987  supinfneg  10012  infsupneg  10013  qmulz  10040  elpq  10067  icc0r  10346  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  ioo0  10712  ico0  10714  ioc0  10715  modqmuladd  10825  addmodlteq  10857  frec2uzrand  10864  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  hashunlem  11267  reuccatpfxs1lem  11541  shftlem  11604  caucvgre  11770  resqrexlemgt0  11809  rexico  12011  negfi  12018  climuni  12085  climshftlemg  12094  climcn1  12100  serf0  12144  summodclem2  12175  zsumdc  12177  fsum2dlemstep  12227  mertenslem2  12329  ntrivcvgap  12341  zproddc  12372  fprod2dlemstep  12415  dvds1lem  12595  odd2np1lem  12665  odd2np1  12666  sqoddm1div8z  12679  ltoddhalfle  12686  halfleoddlt  12687  m1expo  12693  divalglemeunn  12714  divalglemex  12715  divalglemeuneg  12716  flodddiv4  12729  bezoutlemaz  12806  bezoutlembz  12807  dvdssqim  12827  ncoprmgcdne1b  12893  coprmdvds2  12897  divgcdcoprm0  12905  cncongr1  12907  cncongr2  12908  dvdsnprmd  12929  rpexp  12958  pythagtriplem1  13074  pc2dvds  13139  difsqpwdvds  13147  oddprmdvds  13163  prmpwdvds  13164  4sqlem11  13210  imasmnd2  13819  dfgrp3mlem  13963  imasgrp2  13973  issubg4m  14056  imasabl  14231  ringinvnzdiv  14463  imasring  14479  dvdsrcl2  14516  dvdsrmul1  14519  isnzr2  14601  lss1d  14830  lssats2  14861  lspsn  14863  dvdsrzring  15048  znunit  15104  znrrg  15105  tgcl  15302  innei  15401  cnptoprest  15477  lmss  15484  lmtopcnp  15488  txlm  15517  blssps  15665  blss  15666  blssexps  15667  blssex  15668  mopni3  15722  metrest  15744  metcnp3  15749  mulc1cncf  15827  cncfco  15829  elply2  15973  efnthr  16188  gausslemma2dlem1a  16394  lgsquadlem1  16413  2lgsoddprmlem2  16442  uhgrspansubgrlem  16734  pw1ndom3  17237  subctctexmid  17247