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  6590  tfrlemibacc  6602  tfrlemibfn  6604  tfr1onlembacc  6618  tfr1onlembfn  6620  tfrcllembacc  6631  tfrcllembfn  6633  frecabcl  6675  nnaordex  6806  nnawordex  6807  ectocld  6880  phpm  7173  dif1enen  7190  fin0  7195  fin0or  7196  fimax2gtri  7212  fidcenum  7280  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  10011  infsupneg  10012  qmulz  10039  elpq  10066  icc0r  10345  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  ioo0  10711  ico0  10713  ioc0  10714  modqmuladd  10824  addmodlteq  10856  frec2uzrand  10863  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  hashunlem  11266  reuccatpfxs1lem  11540  shftlem  11603  caucvgre  11769  resqrexlemgt0  11808  rexico  12010  negfi  12017  climuni  12084  climshftlemg  12093  climcn1  12099  serf0  12143  summodclem2  12174  zsumdc  12176  fsum2dlemstep  12226  mertenslem2  12328  ntrivcvgap  12340  zproddc  12371  fprod2dlemstep  12414  dvds1lem  12594  odd2np1lem  12664  odd2np1  12665  sqoddm1div8z  12678  ltoddhalfle  12685  halfleoddlt  12686  m1expo  12692  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  flodddiv4  12728  bezoutlemaz  12805  bezoutlembz  12806  dvdssqim  12826  ncoprmgcdne1b  12892  coprmdvds2  12896  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  dvdsnprmd  12928  rpexp  12957  pythagtriplem1  13073  pc2dvds  13138  difsqpwdvds  13146  oddprmdvds  13162  prmpwdvds  13163  4sqlem11  13209  imasmnd2  13818  dfgrp3mlem  13962  imasgrp2  13972  issubg4m  14055  imasabl  14230  ringinvnzdiv  14462  imasring  14478  dvdsrcl2  14515  dvdsrmul1  14518  isnzr2  14600  lss1d  14829  lssats2  14860  lspsn  14862  dvdsrzring  15047  znunit  15103  znrrg  15104  tgcl  15323  innei  15422  cnptoprest  15498  lmss  15505  lmtopcnp  15509  txlm  15538  blssps  15686  blss  15687  blssexps  15688  blssex  15689  mopni3  15743  metrest  15765  metcnp3  15770  mulc1cncf  15848  cncfco  15850  elply2  15994  efnthr  16209  gausslemma2dlem1a  16415  lgsquadlem1  16434  2lgsoddprmlem2  16463  uhgrspansubgrlem  16755  pw1ndom3  17258  subctctexmid  17268