Theorem rexlimiva 3211

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ∃wrex 3066

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070  df-rex 3071

This theorem is referenced by:  rexraleqim  3578  rexopabb  5442  unon  7687  tfrlem16  8233  oawordeulem  8394  nneob  8495  unfi  8964  ominf  9044  unfilem1  9087  pwfiOLD  9123  fival  9180  elfi2  9182  fi0  9188  fiin  9190  djuss  9687  djuun  9693  updjud  9701  finnum  9715  dif1card  9775  fseqenlem2  9790  dfac8alem  9794  alephfp  9873  cflim2  10028  isfin1-3  10151  fin67  10160  isfin7-2  10161  axdc3lem  10215  axdc3lem2  10216  iunfo  10304  iundom2g  10305  winainflem  10458  rankcf  10542  map2psrpr  10875  supsrlem  10876  1re  10984  0re  10986  00id  11159  addid1  11164  0cnALT  11218  om2uzrani  13681  uzrdgfni  13687  wrdf  14231  rexanuz  15066  r19.2uz  15072  fsum2dlem  15491  fsumcom2  15495  fprod2dlem  15699  fprodcom2  15703  0dvds  15995  even2n  16060  m1expe  16092  m1exp1  16094  modprm0  16515  cshwsidrepsw  16804  smndex1basss  18553  smndex1mgm  18555  smndex1mndlem  18557  dfgrp2  18613  psgndiflemA  20815  ppttop  22166  epttop  22168  neips  22273  lmmo  22540  2ndctop  22607  2ndcsep  22619  fbncp  22999  fgcl  23038  filuni  23045  tgioo  23968  zcld  23985  cphsscph  24424  elovolm  24648  nulmbl2  24709  ellimc3  25052  limcflf  25054  pilem3  25621  perfect  26388  2vmadivsum  26698  selberg3lem2  26715  selberg4  26718  pntrsumbnd2  26724  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntpbnd  26745  pnt3  26769  axcontlem12  27352  axcont  27353  clwwlkn1loopb  28416  eleclclwwlkn  28449  uhgr3cyclex  28555  frgrreggt1  28766  norm1exi  29621  nmcexi  30397  lnconi  30404  pjssdif1i  30546  stri  30628  hstri  30636  stcltrthi  30649  shatomici  30729  qsxpid  31567  dispcmp  31818  isrnmeas  32177  dya2iocucvr  32260  sxbrsigalem1  32261  eulerpartlemt  32347  bnj1398  33023  bnj1498  33050  fnrelpredd  33070  satfrnmapom  33341  gonar  33366  goalr  33368  satffun  33380  mthmblem  33551  elno  33858  noreson  33872  nosupbnd1lem5  33924  noinfbnd1lem5  33939  lindsdom  35780  mblfinlem3  35825  ismblfin  35827  volsupnfl  35831  itg2addnclem  35837  itg2addnc  35840  cover2  35881  prtlem16  36890  rexzrexnn0  40633  isnumbasgrplem2  40936  dgraalem  40977  rp-isfinite5  41131  mnurndlem1  41906  grumnudlem  41910  gruex  41923  islptre  43167  stirlinglem13  43634  stirlinglem14  43635  stirling  43637  etransc  43831  ovolval4lem2  44195  sprsymrelf1lem  44954  sprsymrelfolem2  44956  prmdvdsfmtnof  45049  prmdvdsfmtnof1  45050  perfectALTV  45186  tgoldbach  45280  uspgrsprf  45319  2zlidl  45503  2zrngamgm  45508  ply1mulgsumlem1  45738  ply1mulgsumlem2  45739  lincsumcl  45783  lincscmcl  45784  ellcoellss  45787  sepfsepc  46232  seppcld  46234