Theorem rexlimiva 3209

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 412	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 3208	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexraleqim  3569  rexopabb  5434  unon  7653  tfrlem16  8195  oawordeulem  8347  nneob  8446  unfi  8917  ominf  8964  unfilem1  9008  pwfiOLD  9044  fival  9101  elfi2  9103  fi0  9109  fiin  9111  trpredlem1  9405  djuss  9609  djuun  9615  updjud  9623  finnum  9637  dif1card  9697  fseqenlem2  9712  dfac8alem  9716  alephfp  9795  cflim2  9950  isfin1-3  10073  fin67  10082  isfin7-2  10083  axdc3lem  10137  axdc3lem2  10138  iunfo  10226  iundom2g  10227  winainflem  10380  rankcf  10464  map2psrpr  10797  supsrlem  10798  1re  10906  0re  10908  00id  11080  addid1  11085  0cnALT  11139  om2uzrani  13600  uzrdgfni  13606  wrdf  14150  rexanuz  14985  r19.2uz  14991  fsum2dlem  15410  fsumcom2  15414  fprod2dlem  15618  fprodcom2  15622  0dvds  15914  even2n  15979  m1expe  16011  m1exp1  16013  modprm0  16434  cshwsidrepsw  16723  smndex1basss  18459  smndex1mgm  18461  smndex1mndlem  18463  dfgrp2  18519  psgndiflemA  20718  ppttop  22065  epttop  22067  neips  22172  lmmo  22439  2ndctop  22506  2ndcsep  22518  fbncp  22898  fgcl  22937  filuni  22944  tgioo  23865  zcld  23882  cphsscph  24320  elovolm  24544  nulmbl2  24605  ellimc3  24948  limcflf  24950  pilem3  25517  perfect  26284  2vmadivsum  26594  selberg3lem2  26611  selberg4  26614  pntrsumbnd2  26620  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntpbnd  26641  pnt3  26665  axcontlem12  27246  axcont  27247  clwwlkn1loopb  28308  eleclclwwlkn  28341  uhgr3cyclex  28447  frgrreggt1  28658  norm1exi  29513  nmcexi  30289  lnconi  30296  pjssdif1i  30438  stri  30520  hstri  30528  stcltrthi  30541  shatomici  30621  qsxpid  31460  dispcmp  31711  isrnmeas  32068  dya2iocucvr  32151  sxbrsigalem1  32152  eulerpartlemt  32238  bnj1398  32914  bnj1498  32941  fnrelpredd  32961  satfrnmapom  33232  gonar  33257  goalr  33259  satffun  33271  mthmblem  33442  elno  33776  noreson  33790  nosupbnd1lem5  33842  noinfbnd1lem5  33857  lindsdom  35698  mblfinlem3  35743  ismblfin  35745  volsupnfl  35749  itg2addnclem  35755  itg2addnc  35758  cover2  35799  prtlem16  36810  rexzrexnn0  40542  isnumbasgrplem2  40845  dgraalem  40886  rp-isfinite5  41022  mnurndlem1  41788  grumnudlem  41792  gruex  41805  islptre  43050  stirlinglem13  43517  stirlinglem14  43518  stirling  43520  etransc  43714  ovolval4lem2  44078  sprsymrelf1lem  44831  sprsymrelfolem2  44833  prmdvdsfmtnof  44926  prmdvdsfmtnof1  44927  perfectALTV  45063  tgoldbach  45157  uspgrsprf  45196  2zlidl  45380  2zrngamgm  45385  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  lincsumcl  45660  lincscmcl  45661  ellcoellss  45664  sepfsepc  46109  seppcld  46111