Theorem rexlimdva 2662

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∃wrex 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527  df-rex 2528

This theorem is referenced by:  rexlimdvaa  2663  rexlimivv  2668  rexlimdvv  2669  ralxfrd  4588  rexxfrd  4589  fvelimab  5738  foco2  5932  elunirn  5945  f1elima  5952  mpoexw  6422  tfrlem5  6558  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  frecabcl  6643  nnaordex  6774  nnawordex  6775  ectocld  6848  phpm  7133  dif1enen  7150  fin0  7155  fin0or  7156  fimax2gtri  7172  fidcenum  7239  suplub2ti  7305  supisoex  7313  enomnilem  7442  finomni  7444  enmkvlem  7465  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  ltexnqq  7739  ltbtwnnqq  7746  prarloclem4  7829  prarloc2  7835  genprndl  7852  genprndu  7853  prmuloc2  7898  1idprl  7921  1idpru  7922  cauappcvgprlemdisj  7982  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  recexgt0sr  8104  map2psrprg  8136  suplocsrlem  8139  nntopi  8225  cnegexlem1  8464  cnegexlem2  8465  renegcl  8550  aptap  8941  supinfneg  9945  infsupneg  9946  qmulz  9973  elpq  9999  icc0r  10278  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  ioo0  10643  ico0  10645  ioc0  10646  modqmuladd  10752  addmodlteq  10784  frec2uzrand  10791  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  hashunlem  11193  reuccatpfxs1lem  11463  shftlem  11526  caucvgre  11691  resqrexlemgt0  11730  rexico  11931  negfi  11938  climuni  12003  climshftlemg  12012  climcn1  12018  serf0  12062  summodclem2  12093  zsumdc  12095  fsum2dlemstep  12145  mertenslem2  12247  ntrivcvgap  12259  zproddc  12290  fprod2dlemstep  12333  dvds1lem  12513  odd2np1lem  12583  odd2np1  12584  sqoddm1div8z  12597  ltoddhalfle  12604  halfleoddlt  12605  m1expo  12611  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  flodddiv4  12647  bezoutlemaz  12724  bezoutlembz  12725  dvdssqim  12745  ncoprmgcdne1b  12811  coprmdvds2  12815  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  dvdsnprmd  12847  rpexp  12875  pythagtriplem1  12988  pc2dvds  13053  difsqpwdvds  13061  oddprmdvds  13077  prmpwdvds  13078  4sqlem11  13124  imasmnd2  13749  dfgrp3mlem  13895  imasgrp2  13911  issubg4m  13994  imasabl  14137  ringinvnzdiv  14278  imasring  14292  dvdsrcl2  14329  dvdsrmul1  14332  isnzr2  14414  lss1d  14643  lssats2  14674  lspsn  14676  dvdsrzring  14863  znunit  14919  znrrg  14920  tgcl  15041  innei  15140  cnptoprest  15216  lmss  15223  lmtopcnp  15227  txlm  15256  blssps  15404  blss  15405  blssexps  15406  blssex  15407  mopni3  15461  metrest  15483  metcnp3  15488  mulc1cncf  15566  cncfco  15568  elply2  15712  gausslemma2dlem1a  16043  lgsquadlem1  16062  2lgsoddprmlem2  16091  uhgrspansubgrlem  16383  pw1ndom3  16876  subctctexmid  16886