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  7342  supisoex  7350  enomnilem  7479  finomni  7481  enmkvlem  7502  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  ltexnqq  7776  ltbtwnnqq  7783  prarloclem4  7866  prarloc2  7872  genprndl  7889  genprndu  7890  prmuloc2  7935  1idprl  7958  1idpru  7959  cauappcvgprlemdisj  8019  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  recexgt0sr  8141  map2psrprg  8173  suplocsrlem  8176  nntopi  8262  cnegexlem1  8503  cnegexlem2  8504  renegcl  8589  aptap  8981  supinfneg  10005  infsupneg  10006  qmulz  10033  elpq  10060  icc0r  10339  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  ioo0  10705  ico0  10707  ioc0  10708  modqmuladd  10817  addmodlteq  10849  frec2uzrand  10856  frecuzrdgtcl  10863  frecuzrdgfunlem  10870  hashunlem  11259  reuccatpfxs1lem  11533  shftlem  11596  caucvgre  11762  resqrexlemgt0  11801  rexico  12003  negfi  12010  climuni  12077  climshftlemg  12086  climcn1  12092  serf0  12136  summodclem2  12167  zsumdc  12169  fsum2dlemstep  12219  mertenslem2  12321  ntrivcvgap  12333  zproddc  12364  fprod2dlemstep  12407  dvds1lem  12587  odd2np1lem  12657  odd2np1  12658  sqoddm1div8z  12671  ltoddhalfle  12678  halfleoddlt  12679  m1expo  12685  divalglemeunn  12706  divalglemex  12707  divalglemeuneg  12708  flodddiv4  12721  bezoutlemaz  12798  bezoutlembz  12799  dvdssqim  12819  ncoprmgcdne1b  12885  coprmdvds2  12889  divgcdcoprm0  12897  cncongr1  12899  cncongr2  12900  dvdsnprmd  12921  rpexp  12950  pythagtriplem1  13066  pc2dvds  13131  difsqpwdvds  13139  oddprmdvds  13155  prmpwdvds  13156  4sqlem11  13202  imasmnd2  13810  dfgrp3mlem  13954  imasgrp2  13964  issubg4m  14047  imasabl  14191  ringinvnzdiv  14406  imasring  14420  dvdsrcl2  14457  dvdsrmul1  14460  isnzr2  14542  lss1d  14771  lssats2  14802  lspsn  14804  dvdsrzring  14989  znunit  15045  znrrg  15046  tgcl  15217  innei  15316  cnptoprest  15392  lmss  15399  lmtopcnp  15403  txlm  15432  blssps  15580  blss  15581  blssexps  15582  blssex  15583  mopni3  15637  metrest  15659  metcnp3  15664  mulc1cncf  15742  cncfco  15744  elply2  15888  gausslemma2dlem1a  16299  lgsquadlem1  16318  2lgsoddprmlem2  16347  uhgrspansubgrlem  16639  pw1ndom3  17142  subctctexmid  17152