Theorem rexlimiva 3283

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)

Hypothesis

Ref	Expression
rexlimiva.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
rexlimiva	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
2	1	ex 415	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 3282	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  rexraleqim  3642  rexopabb  5417  unon  7548  tfrlem16  8031  oawordeulem  8182  nneob  8281  ominf  8732  unfilem1  8784  pwfi  8821  fival  8878  elfi2  8880  fi0  8886  fiin  8888  djuss  9351  djuun  9357  updjud  9365  finnum  9379  dif1card  9438  fseqenlem2  9453  dfac8alem  9457  alephfp  9536  cflim2  9687  isfin1-3  9810  fin67  9819  isfin7-2  9820  axdc3lem  9874  axdc3lem2  9875  iunfo  9963  iundom2g  9964  winainflem  10117  rankcf  10201  map2psrpr  10534  supsrlem  10535  1re  10643  0re  10645  00id  10817  addid1  10822  0cnALT  10876  om2uzrani  13323  uzrdgfni  13329  wrdf  13869  rexanuz  14707  r19.2uz  14713  fsum2dlem  15127  fsumcom2  15131  fprod2dlem  15336  fprodcom2  15340  0dvds  15632  even2n  15693  m1expe  15727  m1exp1  15729  modprm0  16144  cshwsidrepsw  16429  smndex1basss  18072  smndex1mgm  18074  smndex1mndlem  18076  dfgrp2  18130  psgndiflemA  20747  ppttop  21617  epttop  21619  neips  21723  lmmo  21990  2ndctop  22057  2ndcsep  22069  fbncp  22449  fgcl  22488  filuni  22495  tgioo  23406  zcld  23423  cphsscph  23856  elovolm  24078  nulmbl2  24139  ellimc3  24479  limcflf  24481  pilem3  25043  perfect  25809  2vmadivsum  26119  selberg3lem2  26136  selberg4  26139  pntrsumbnd2  26145  pntrlog2bndlem3  26157  pntrlog2bndlem4  26158  pntpbnd  26166  pnt3  26190  axcontlem12  26763  axcont  26764  clwwlkn1loopb  27823  eleclclwwlkn  27857  uhgr3cyclex  27963  frgrreggt1  28174  norm1exi  29029  nmcexi  29805  lnconi  29812  pjssdif1i  29954  stri  30036  hstri  30044  stcltrthi  30057  shatomici  30137  qsxpid  30929  dispcmp  31125  isrnmeas  31461  dya2iocucvr  31544  sxbrsigalem1  31545  eulerpartlemt  31631  bnj1398  32308  bnj1498  32335  satfrnmapom  32619  gonar  32644  goalr  32646  satffun  32658  mthmblem  32829  trpredlem1  33068  elno  33155  noreson  33169  nosupbnd1lem5  33214  lindsdom  34888  mblfinlem3  34933  ismblfin  34935  volsupnfl  34939  itg2addnclem  34945  itg2addnc  34948  cover2  34991  prtlem16  36007  rexzrexnn0  39408  isnumbasgrplem2  39711  dgraalem  39752  rp-isfinite5  39890  mnurndlem1  40624  grumnudlem  40628  gruex  40641  islptre  41907  stirlinglem13  42378  stirlinglem14  42379  stirling  42381  etransc  42575  ovolval4lem2  42939  sprsymrelf1lem  43660  sprsymrelfolem2  43662  prmdvdsfmtnof  43755  prmdvdsfmtnof1  43756  perfectALTV  43895  tgoldbach  43989  uspgrsprf  44028  2zlidl  44212  2zrngamgm  44217  ply1mulgsumlem1  44447  ply1mulgsumlem2  44448  lincsumcl  44493  lincscmcl  44494  ellcoellss  44497