Theorem rexlimdva 2648

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdvaa  2649  rexlimivv  2654  rexlimdvv  2655  ralxfrd  4554  rexxfrd  4555  fvelimab  5695  foco2  5886  elunirn  5899  f1elima  5906  mpoexw  6370  tfrlem5  6471  tfrlemibacc  6483  tfrlemibfn  6485  tfr1onlembacc  6499  tfr1onlembfn  6501  tfrcllembacc  6512  tfrcllembfn  6514  frecabcl  6556  nnaordex  6687  nnawordex  6688  ectocld  6761  phpm  7040  dif1enen  7055  fin0  7060  fin0or  7061  fimax2gtri  7077  fidcenum  7139  suplub2ti  7184  supisoex  7192  enomnilem  7321  finomni  7323  enmkvlem  7344  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  ltexnqq  7611  ltbtwnnqq  7618  prarloclem4  7701  prarloc2  7707  genprndl  7724  genprndu  7725  prmuloc2  7770  1idprl  7793  1idpru  7794  cauappcvgprlemdisj  7854  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  recexgt0sr  7976  map2psrprg  8008  suplocsrlem  8011  nntopi  8097  cnegexlem1  8337  cnegexlem2  8338  renegcl  8423  aptap  8813  supinfneg  9807  infsupneg  9808  qmulz  9835  elpq  9861  icc0r  10139  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  ioo0  10496  ico0  10498  ioc0  10499  modqmuladd  10605  addmodlteq  10637  frec2uzrand  10644  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  hashunlem  11043  reuccatpfxs1lem  11299  shftlem  11348  caucvgre  11513  resqrexlemgt0  11552  rexico  11753  negfi  11760  climuni  11825  climshftlemg  11834  climcn1  11840  serf0  11884  summodclem2  11914  zsumdc  11916  fsum2dlemstep  11966  mertenslem2  12068  ntrivcvgap  12080  zproddc  12111  fprod2dlemstep  12154  dvds1lem  12334  odd2np1lem  12404  odd2np1  12405  sqoddm1div8z  12418  ltoddhalfle  12425  halfleoddlt  12426  m1expo  12432  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  flodddiv4  12468  bezoutlemaz  12545  bezoutlembz  12546  dvdssqim  12566  ncoprmgcdne1b  12632  coprmdvds2  12636  divgcdcoprm0  12644  cncongr1  12646  cncongr2  12647  dvdsnprmd  12668  rpexp  12696  pythagtriplem1  12809  pc2dvds  12874  difsqpwdvds  12882  oddprmdvds  12898  prmpwdvds  12899  4sqlem11  12945  imasmnd2  13506  dfgrp3mlem  13652  imasgrp2  13668  issubg4m  13751  imasabl  13894  ringinvnzdiv  14034  imasring  14048  dvdsrcl2  14084  dvdsrmul1  14087  isnzr2  14169  lss1d  14368  lssats2  14399  lspsn  14401  dvdsrzring  14588  znunit  14644  znrrg  14645  tgcl  14759  innei  14858  cnptoprest  14934  lmss  14941  lmtopcnp  14945  txlm  14974  blssps  15122  blss  15123  blssexps  15124  blssex  15125  mopni3  15179  metrest  15201  metcnp3  15206  mulc1cncf  15284  cncfco  15286  elply2  15430  gausslemma2dlem1a  15758  lgsquadlem1  15777  2lgsoddprmlem2  15806  pw1ndom3  16467  subctctexmid  16479