Theorem rexlimiva 3284

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ∃wrex 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  rexraleqim  3643  rexopabb  5418  unon  7549  tfrlem16  8032  oawordeulem  8183  nneob  8282  ominf  8733  unfilem1  8785  pwfi  8822  fival  8879  elfi2  8881  fi0  8887  fiin  8889  djuss  9352  djuun  9358  updjud  9366  finnum  9380  dif1card  9439  fseqenlem2  9454  dfac8alem  9458  alephfp  9537  cflim2  9688  isfin1-3  9811  fin67  9820  isfin7-2  9821  axdc3lem  9875  axdc3lem2  9876  iunfo  9964  iundom2g  9965  winainflem  10118  rankcf  10202  map2psrpr  10535  supsrlem  10536  1re  10644  0re  10646  00id  10818  addid1  10823  0cnALT  10877  om2uzrani  13323  uzrdgfni  13329  wrdf  13869  rexanuz  14708  r19.2uz  14714  fsum2dlem  15128  fsumcom2  15132  fprod2dlem  15337  fprodcom2  15341  0dvds  15633  even2n  15694  m1expe  15728  m1exp1  15730  modprm0  16145  cshwsidrepsw  16430  smndex1basss  18073  smndex1mgm  18075  smndex1mndlem  18077  dfgrp2  18131  psgndiflemA  20748  ppttop  21618  epttop  21620  neips  21724  lmmo  21991  2ndctop  22058  2ndcsep  22070  fbncp  22450  fgcl  22489  filuni  22496  tgioo  23407  zcld  23424  cphsscph  23857  elovolm  24079  nulmbl2  24140  ellimc3  24480  limcflf  24482  pilem3  25044  perfect  25810  2vmadivsum  26120  selberg3lem2  26137  selberg4  26140  pntrsumbnd2  26146  pntrlog2bndlem3  26158  pntrlog2bndlem4  26159  pntpbnd  26167  pnt3  26191  axcontlem12  26764  axcont  26765  clwwlkn1loopb  27824  eleclclwwlkn  27858  uhgr3cyclex  27964  frgrreggt1  28175  norm1exi  29030  nmcexi  29806  lnconi  29813  pjssdif1i  29955  stri  30037  hstri  30045  stcltrthi  30058  shatomici  30138  qsxpid  30931  dispcmp  31127  isrnmeas  31463  dya2iocucvr  31546  sxbrsigalem1  31547  eulerpartlemt  31633  bnj1398  32310  bnj1498  32337  satfrnmapom  32621  gonar  32646  goalr  32648  satffun  32660  mthmblem  32831  trpredlem1  33070  elno  33157  noreson  33171  nosupbnd1lem5  33216  lindsdom  34890  mblfinlem3  34935  ismblfin  34937  volsupnfl  34941  itg2addnclem  34947  itg2addnc  34950  cover2  34993  prtlem16  36009  rexzrexnn0  39407  isnumbasgrplem2  39710  dgraalem  39751  rp-isfinite5  39889  mnurndlem1  40623  grumnudlem  40627  gruex  40640  islptre  41906  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