Theorem rexlimiva 3212

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

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

This theorem is referenced by:  rexraleqim  3578  rexopabb  5443  unon  7670  tfrlem16  8213  oawordeulem  8368  nneob  8467  unfi  8935  ominf  9011  unfilem1  9054  pwfiOLD  9090  fival  9147  elfi2  9149  fi0  9155  fiin  9157  trpredlem1  9472  djuss  9677  djuun  9683  updjud  9691  finnum  9705  dif1card  9765  fseqenlem2  9780  dfac8alem  9784  alephfp  9863  cflim2  10018  isfin1-3  10141  fin67  10150  isfin7-2  10151  axdc3lem  10205  axdc3lem2  10206  iunfo  10294  iundom2g  10295  winainflem  10448  rankcf  10532  map2psrpr  10865  supsrlem  10866  1re  10974  0re  10976  00id  11148  addid1  11153  0cnALT  11207  om2uzrani  13668  uzrdgfni  13674  wrdf  14218  rexanuz  15053  r19.2uz  15059  fsum2dlem  15478  fsumcom2  15482  fprod2dlem  15686  fprodcom2  15690  0dvds  15982  even2n  16047  m1expe  16079  m1exp1  16081  modprm0  16502  cshwsidrepsw  16791  smndex1basss  18540  smndex1mgm  18542  smndex1mndlem  18544  dfgrp2  18600  psgndiflemA  20802  ppttop  22153  epttop  22155  neips  22260  lmmo  22527  2ndctop  22594  2ndcsep  22606  fbncp  22986  fgcl  23025  filuni  23032  tgioo  23955  zcld  23972  cphsscph  24411  elovolm  24635  nulmbl2  24696  ellimc3  25039  limcflf  25041  pilem3  25608  perfect  26375  2vmadivsum  26685  selberg3lem2  26702  selberg4  26705  pntrsumbnd2  26711  pntrlog2bndlem3  26723  pntrlog2bndlem4  26724  pntpbnd  26732  pnt3  26756  axcontlem12  27339  axcont  27340  clwwlkn1loopb  28401  eleclclwwlkn  28434  uhgr3cyclex  28540  frgrreggt1  28751  norm1exi  29606  nmcexi  30382  lnconi  30389  pjssdif1i  30531  stri  30613  hstri  30621  stcltrthi  30634  shatomici  30714  qsxpid  31552  dispcmp  31803  isrnmeas  32162  dya2iocucvr  32245  sxbrsigalem1  32246  eulerpartlemt  32332  bnj1398  33008  bnj1498  33035  fnrelpredd  33055  satfrnmapom  33326  gonar  33351  goalr  33353  satffun  33365  mthmblem  33536  elno  33843  noreson  33857  nosupbnd1lem5  33909  noinfbnd1lem5  33924  lindsdom  35765  mblfinlem3  35810  ismblfin  35812  volsupnfl  35816  itg2addnclem  35822  itg2addnc  35825  cover2  35866  prtlem16  36877  rexzrexnn0  40621  isnumbasgrplem2  40924  dgraalem  40965  rp-isfinite5  41101  mnurndlem1  41867  grumnudlem  41871  gruex  41884  islptre  43129  stirlinglem13  43596  stirlinglem14  43597  stirling  43599  etransc  43793  ovolval4lem2  44157  sprsymrelf1lem  44910  sprsymrelfolem2  44912  prmdvdsfmtnof  45005  prmdvdsfmtnof1  45006  perfectALTV  45142  tgoldbach  45236  uspgrsprf  45275  2zlidl  45459  2zrngamgm  45464  ply1mulgsumlem1  45694  ply1mulgsumlem2  45695  lincsumcl  45739  lincscmcl  45740  ellcoellss  45743  sepfsepc  46188  seppcld  46190