Theorem rexlimiva 3122

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 3054	. 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 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  rexlimiv  3123  rexlimivw  3126  rexraleqim  3602  rexopabb  5471  unon  7764  tfrlem16  8315  oawordeulem  8472  nneob  8574  unfi  9085  ominf  9153  unfilem1  9194  fival  9302  elfi2  9304  fi0  9310  fiin  9312  djuss  9816  djuun  9822  updjud  9830  finnum  9844  dif1card  9904  fseqenlem2  9919  dfac8alem  9923  alephfp  10002  cflim2  10157  isfin1-3  10280  fin67  10289  isfin7-2  10290  axdc3lem  10344  axdc3lem2  10345  iunfo  10433  iundom2g  10434  winainflem  10587  rankcf  10671  map2psrpr  11004  supsrlem  11005  1re  11115  0re  11117  00id  11291  addrid  11296  0cnALT  11351  om2uzrani  13859  uzrdgfni  13865  wrdf  14425  rexanuz  15253  r19.2uz  15259  fsum2dlem  15677  fsumcom2  15681  fprod2dlem  15887  fprodcom2  15891  0dvds  16187  even2n  16253  m1expe  16285  m1exp1  16287  modprm0  16717  cshwsidrepsw  17005  smndex1basss  18779  smndex1mgm  18781  smndex1mndlem  18783  dfgrp2  18841  pzriprnglem4  21391  psgndiflemA  21508  ppttop  22892  epttop  22894  neips  22998  lmmo  23265  2ndctop  23332  2ndcsep  23344  fbncp  23724  fgcl  23763  filuni  23770  tgioo  24682  zcld  24700  cphsscph  25149  elovolm  25374  nulmbl2  25435  ellimc3  25778  limcflf  25780  pilem3  26361  perfect  27140  2vmadivsum  27450  selberg3lem2  27467  selberg4  27470  pntrsumbnd2  27476  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntpbnd  27497  pnt3  27521  elnoOLD  27556  noreson  27570  nosupbnd1lem5  27622  noinfbnd1lem5  27637  axcontlem12  28920  axcont  28921  clwwlkn1loopb  29987  eleclclwwlkn  30020  uhgr3cyclex  30126  frgrreggt1  30337  norm1exi  31194  nmcexi  31970  lnconi  31977  pjssdif1i  32119  stri  32201  hstri  32209  stcltrthi  32222  shatomici  32302  qsxpid  33299  dispcmp  33826  isrnmeas  34167  dya2iocucvr  34252  sxbrsigalem1  34253  eulerpartlemt  34339  bnj1398  35001  bnj1498  35028  fnrelpredd  35056  wevgblacfn  35086  satfrnmapom  35347  gonar  35372  goalr  35374  satffun  35386  mthmblem  35557  lindsdom  37598  mblfinlem3  37643  ismblfin  37645  volsupnfl  37649  itg2addnclem  37655  itg2addnc  37658  cover2  37699  prtlem16  38852  rexzrexnn0  42781  isnumbasgrplem2  43081  dgraalem  43122  onsucrn  43248  dflim5  43306  dfno2  43405  rp-isfinite5  43494  mnurndlem1  44258  grumnudlem  44262  gruex  44275  islptre  45604  stirlinglem13  46071  stirlinglem14  46072  stirling  46074  etransc  46268  ovolval4lem2  46635  sprsymrelf1lem  47479  sprsymrelfolem2  47481  prmdvdsfmtnof  47574  prmdvdsfmtnof1  47575  perfectALTV  47711  tgoldbach  47805  uspgrsprf  48134  2zlidl  48228  2zrngamgm  48233  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  lincsumcl  48420  lincscmcl  48421  ellcoellss  48424  sepfsepc  48916  seppcld  48918