Theorem rexlimiva 3147

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝜓,𝑥

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

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1930	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
4	1, 3	sylbi 217	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

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 207  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexlimiv  3148  rexlimivw  3151  rexraleqim  3647  rexopabb  5533  unon  7851  tfrlem16  8433  oawordeulem  8592  nneob  8694  unfi  9211  ominf  9294  ominfOLD  9295  unfilem1  9343  fival  9452  elfi2  9454  fi0  9460  fiin  9462  djuss  9960  djuun  9966  updjud  9974  finnum  9988  dif1card  10050  fseqenlem2  10065  dfac8alem  10069  alephfp  10148  cflim2  10303  isfin1-3  10426  fin67  10435  isfin7-2  10436  axdc3lem  10490  axdc3lem2  10491  iunfo  10579  iundom2g  10580  winainflem  10733  rankcf  10817  map2psrpr  11150  supsrlem  11151  1re  11261  0re  11263  00id  11436  addrid  11441  0cnALT  11496  om2uzrani  13993  uzrdgfni  13999  wrdf  14557  rexanuz  15384  r19.2uz  15390  fsum2dlem  15806  fsumcom2  15810  fprod2dlem  16016  fprodcom2  16020  0dvds  16314  even2n  16379  m1expe  16411  m1exp1  16413  modprm0  16843  cshwsidrepsw  17131  smndex1basss  18918  smndex1mgm  18920  smndex1mndlem  18922  dfgrp2  18980  pzriprnglem4  21495  psgndiflemA  21619  ppttop  23014  epttop  23016  neips  23121  lmmo  23388  2ndctop  23455  2ndcsep  23467  fbncp  23847  fgcl  23886  filuni  23893  tgioo  24817  zcld  24835  cphsscph  25285  elovolm  25510  nulmbl2  25571  ellimc3  25914  limcflf  25916  pilem3  26497  perfect  27275  2vmadivsum  27585  selberg3lem2  27602  selberg4  27605  pntrsumbnd2  27611  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntpbnd  27632  pnt3  27656  elnoOLD  27691  noreson  27705  nosupbnd1lem5  27757  noinfbnd1lem5  27772  axcontlem12  28990  axcont  28991  clwwlkn1loopb  30062  eleclclwwlkn  30095  uhgr3cyclex  30201  frgrreggt1  30412  norm1exi  31269  nmcexi  32045  lnconi  32052  pjssdif1i  32194  stri  32276  hstri  32284  stcltrthi  32297  shatomici  32377  qsxpid  33390  dispcmp  33858  isrnmeas  34201  dya2iocucvr  34286  sxbrsigalem1  34287  eulerpartlemt  34373  bnj1398  35048  bnj1498  35075  fnrelpredd  35103  wevgblacfn  35114  satfrnmapom  35375  gonar  35400  goalr  35402  satffun  35414  mthmblem  35585  lindsdom  37621  mblfinlem3  37666  ismblfin  37668  volsupnfl  37672  itg2addnclem  37678  itg2addnc  37681  cover2  37722  prtlem16  38870  rexzrexnn0  42815  isnumbasgrplem2  43116  dgraalem  43157  onsucrn  43284  dflim5  43342  dfno2  43441  rp-isfinite5  43530  mnurndlem1  44300  grumnudlem  44304  gruex  44317  islptre  45634  stirlinglem13  46101  stirlinglem14  46102  stirling  46104  etransc  46298  ovolval4lem2  46665  sprsymrelf1lem  47478  sprsymrelfolem2  47480  prmdvdsfmtnof  47573  prmdvdsfmtnof1  47574  perfectALTV  47710  tgoldbach  47804  uspgrsprf  48062  2zlidl  48156  2zrngamgm  48161  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  lincsumcl  48348  lincscmcl  48349  ellcoellss  48352  sepfsepc  48825  seppcld  48827