Theorem rexlimdva 2594

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  rexlimdvaa  2595  rexlimivv  2600  rexlimdvv  2601  ralxfrd  4463  rexxfrd  4464  fvelimab  5573  foco2  5755  elunirn  5767  f1elima  5774  mpoexw  6214  tfrlem5  6315  tfrlemibacc  6327  tfrlemibfn  6329  tfr1onlembacc  6343  tfr1onlembfn  6345  tfrcllembacc  6356  tfrcllembfn  6358  frecabcl  6400  nnaordex  6529  nnawordex  6530  ectocld  6601  phpm  6865  dif1enen  6880  fin0  6885  fin0or  6886  fimax2gtri  6901  fidcenum  6955  suplub2ti  7000  supisoex  7008  enomnilem  7136  finomni  7138  enmkvlem  7159  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  ltexnqq  7407  ltbtwnnqq  7414  prarloclem4  7497  prarloc2  7503  genprndl  7520  genprndu  7521  prmuloc2  7566  1idprl  7589  1idpru  7590  cauappcvgprlemdisj  7650  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  recexgt0sr  7772  map2psrprg  7804  suplocsrlem  7807  nntopi  7893  cnegexlem1  8132  cnegexlem2  8133  renegcl  8218  aptap  8607  supinfneg  9595  infsupneg  9596  qmulz  9623  elpq  9648  icc0r  9926  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  ioo0  10260  ico0  10262  ioc0  10263  modqmuladd  10366  addmodlteq  10398  frec2uzrand  10405  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  hashunlem  10784  shftlem  10825  caucvgre  10990  resqrexlemgt0  11029  rexico  11230  negfi  11236  climuni  11301  climshftlemg  11310  climcn1  11316  serf0  11360  summodclem2  11390  zsumdc  11392  fsum2dlemstep  11442  mertenslem2  11544  ntrivcvgap  11556  zproddc  11587  fprod2dlemstep  11630  dvds1lem  11809  odd2np1lem  11877  odd2np1  11878  sqoddm1div8z  11891  ltoddhalfle  11898  halfleoddlt  11899  m1expo  11905  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  flodddiv4  11939  bezoutlemaz  12004  bezoutlembz  12005  dvdssqim  12025  ncoprmgcdne1b  12089  coprmdvds2  12093  divgcdcoprm0  12101  cncongr1  12103  cncongr2  12104  dvdsnprmd  12125  rpexp  12153  pythagtriplem1  12265  pc2dvds  12329  difsqpwdvds  12337  oddprmdvds  12352  prmpwdvds  12353  dfgrp3mlem  12968  issubg4m  13053  ringinvnzdiv  13227  dvdsrcl2  13268  dvdsrmul1  13271  dvdsrzring  13496  tgcl  13567  innei  13666  cnptoprest  13742  lmss  13749  lmtopcnp  13753  txlm  13782  blssps  13930  blss  13931  blssexps  13932  blssex  13933  mopni3  13987  metrest  14009  metcnp3  14014  mulc1cncf  14079  cncfco  14081  2lgsoddprmlem2  14457  subctctexmid  14753