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  4557  rexxfrd  4558  fvelimab  5698  foco2  5889  elunirn  5902  f1elima  5909  mpoexw  6373  tfrlem5  6475  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  frecabcl  6560  nnaordex  6691  nnawordex  6692  ectocld  6765  phpm  7047  dif1enen  7064  fin0  7069  fin0or  7070  fimax2gtri  7086  fidcenum  7149  suplub2ti  7194  supisoex  7202  enomnilem  7331  finomni  7333  enmkvlem  7354  exmidfodomrlemeldju  7403  exmidfodomrlemreseldju  7404  ltexnqq  7621  ltbtwnnqq  7628  prarloclem4  7711  prarloc2  7717  genprndl  7734  genprndu  7735  prmuloc2  7780  1idprl  7803  1idpru  7804  cauappcvgprlemdisj  7864  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  recexgt0sr  7986  map2psrprg  8018  suplocsrlem  8021  nntopi  8107  cnegexlem1  8347  cnegexlem2  8348  renegcl  8433  aptap  8823  supinfneg  9822  infsupneg  9823  qmulz  9850  elpq  9876  icc0r  10154  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  ioo0  10512  ico0  10514  ioc0  10515  modqmuladd  10621  addmodlteq  10653  frec2uzrand  10660  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  hashunlem  11060  reuccatpfxs1lem  11320  shftlem  11370  caucvgre  11535  resqrexlemgt0  11574  rexico  11775  negfi  11782  climuni  11847  climshftlemg  11856  climcn1  11862  serf0  11906  summodclem2  11936  zsumdc  11938  fsum2dlemstep  11988  mertenslem2  12090  ntrivcvgap  12102  zproddc  12133  fprod2dlemstep  12176  dvds1lem  12356  odd2np1lem  12426  odd2np1  12427  sqoddm1div8z  12440  ltoddhalfle  12447  halfleoddlt  12448  m1expo  12454  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  flodddiv4  12490  bezoutlemaz  12567  bezoutlembz  12568  dvdssqim  12588  ncoprmgcdne1b  12654  coprmdvds2  12658  divgcdcoprm0  12666  cncongr1  12668  cncongr2  12669  dvdsnprmd  12690  rpexp  12718  pythagtriplem1  12831  pc2dvds  12896  difsqpwdvds  12904  oddprmdvds  12920  prmpwdvds  12921  4sqlem11  12967  imasmnd2  13528  dfgrp3mlem  13674  imasgrp2  13690  issubg4m  13773  imasabl  13916  ringinvnzdiv  14056  imasring  14070  dvdsrcl2  14106  dvdsrmul1  14109  isnzr2  14191  lss1d  14390  lssats2  14421  lspsn  14423  dvdsrzring  14610  znunit  14666  znrrg  14667  tgcl  14781  innei  14880  cnptoprest  14956  lmss  14963  lmtopcnp  14967  txlm  14996  blssps  15144  blss  15145  blssexps  15146  blssex  15147  mopni3  15201  metrest  15223  metcnp3  15228  mulc1cncf  15306  cncfco  15308  elply2  15452  gausslemma2dlem1a  15780  lgsquadlem1  15799  2lgsoddprmlem2  15828  pw1ndom3  16539  subctctexmid  16551