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  4608  rexxfrd  4609  fvelimab  5759  foco2  5959  elunirn  5972  f1elima  5979  mpoexw  6449  tfrlem5  6585  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  frecabcl  6670  nnaordex  6801  nnawordex  6802  ectocld  6875  phpm  7167  dif1enen  7184  fin0  7189  fin0or  7190  fimax2gtri  7206  fidcenum  7273  suplub2ti  7341  supisoex  7349  enomnilem  7478  finomni  7480  enmkvlem  7501  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  ltexnqq  7775  ltbtwnnqq  7782  prarloclem4  7865  prarloc2  7871  genprndl  7888  genprndu  7889  prmuloc2  7934  1idprl  7957  1idpru  7958  cauappcvgprlemdisj  8018  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  recexgt0sr  8140  map2psrprg  8172  suplocsrlem  8175  nntopi  8261  cnegexlem1  8501  cnegexlem2  8502  renegcl  8587  aptap  8979  supinfneg  9997  infsupneg  9998  qmulz  10025  elpq  10051  icc0r  10330  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  ioo0  10696  ico0  10698  ioc0  10699  modqmuladd  10805  addmodlteq  10837  frec2uzrand  10844  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  hashunlem  11246  reuccatpfxs1lem  11520  shftlem  11583  caucvgre  11749  resqrexlemgt0  11788  rexico  11989  negfi  11996  climuni  12061  climshftlemg  12070  climcn1  12076  serf0  12120  summodclem2  12151  zsumdc  12153  fsum2dlemstep  12203  mertenslem2  12305  ntrivcvgap  12317  zproddc  12348  fprod2dlemstep  12391  dvds1lem  12571  odd2np1lem  12641  odd2np1  12642  sqoddm1div8z  12655  ltoddhalfle  12662  halfleoddlt  12663  m1expo  12669  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  flodddiv4  12705  bezoutlemaz  12782  bezoutlembz  12783  dvdssqim  12803  ncoprmgcdne1b  12869  coprmdvds2  12873  divgcdcoprm0  12881  cncongr1  12883  cncongr2  12884  dvdsnprmd  12905  rpexp  12933  pythagtriplem1  13046  pc2dvds  13111  difsqpwdvds  13119  oddprmdvds  13135  prmpwdvds  13136  4sqlem11  13182  imasmnd2  13761  dfgrp3mlem  13905  imasgrp2  13915  issubg4m  13998  imasabl  14142  ringinvnzdiv  14357  imasring  14371  dvdsrcl2  14408  dvdsrmul1  14411  isnzr2  14493  lss1d  14722  lssats2  14753  lspsn  14755  dvdsrzring  14940  znunit  14996  znrrg  14997  tgcl  15167  innei  15266  cnptoprest  15342  lmss  15349  lmtopcnp  15353  txlm  15382  blssps  15530  blss  15531  blssexps  15532  blssex  15533  mopni3  15587  metrest  15609  metcnp3  15614  mulc1cncf  15692  cncfco  15694  elply2  15838  gausslemma2dlem1a  16189  lgsquadlem1  16208  2lgsoddprmlem2  16237  uhgrspansubgrlem  16529  pw1ndom3  17032  subctctexmid  17042