Theorem rexlimiva 3148

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 3072	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1934	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
4	1, 3	sylbi 216	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

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-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimiv  3149  rexlimivw  3152  rexraleqim  3636  rexopabb  5529  unon  7819  tfrlem16  8393  oawordeulem  8554  nneob  8655  unfi  9172  ominf  9258  ominfOLD  9259  unfilem1  9310  pwfiOLD  9347  fival  9407  elfi2  9409  fi0  9415  fiin  9417  djuss  9915  djuun  9921  updjud  9929  finnum  9943  dif1card  10005  fseqenlem2  10020  dfac8alem  10024  alephfp  10103  cflim2  10258  isfin1-3  10381  fin67  10390  isfin7-2  10391  axdc3lem  10445  axdc3lem2  10446  iunfo  10534  iundom2g  10535  winainflem  10688  rankcf  10772  map2psrpr  11105  supsrlem  11106  1re  11214  0re  11216  00id  11389  addrid  11394  0cnALT  11448  om2uzrani  13917  uzrdgfni  13923  wrdf  14469  rexanuz  15292  r19.2uz  15298  fsum2dlem  15716  fsumcom2  15720  fprod2dlem  15924  fprodcom2  15928  0dvds  16220  even2n  16285  m1expe  16317  m1exp1  16319  modprm0  16738  cshwsidrepsw  17027  smndex1basss  18786  smndex1mgm  18788  smndex1mndlem  18790  dfgrp2  18847  psgndiflemA  21154  ppttop  22510  epttop  22512  neips  22617  lmmo  22884  2ndctop  22951  2ndcsep  22963  fbncp  23343  fgcl  23382  filuni  23389  tgioo  24312  zcld  24329  cphsscph  24768  elovolm  24992  nulmbl2  25053  ellimc3  25396  limcflf  25398  pilem3  25965  perfect  26734  2vmadivsum  27044  selberg3lem2  27061  selberg4  27064  pntrsumbnd2  27070  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntpbnd  27091  pnt3  27115  elno  27149  noreson  27163  nosupbnd1lem5  27215  noinfbnd1lem5  27230  axcontlem12  28233  axcont  28234  clwwlkn1loopb  29296  eleclclwwlkn  29329  uhgr3cyclex  29435  frgrreggt1  29646  norm1exi  30503  nmcexi  31279  lnconi  31286  pjssdif1i  31428  stri  31510  hstri  31518  stcltrthi  31531  shatomici  31611  qsxpid  32474  dispcmp  32839  isrnmeas  33198  dya2iocucvr  33283  sxbrsigalem1  33284  eulerpartlemt  33370  bnj1398  34045  bnj1498  34072  fnrelpredd  34092  satfrnmapom  34361  gonar  34386  goalr  34388  satffun  34400  mthmblem  34571  lindsdom  36482  mblfinlem3  36527  ismblfin  36529  volsupnfl  36533  itg2addnclem  36539  itg2addnc  36542  cover2  36583  prtlem16  37739  rexzrexnn0  41542  isnumbasgrplem2  41846  dgraalem  41887  onsucrn  42021  dflim5  42079  dfno2  42179  rp-isfinite5  42268  mnurndlem1  43040  grumnudlem  43044  gruex  43057  islptre  44335  stirlinglem13  44802  stirlinglem14  44803  stirling  44805  etransc  44999  ovolval4lem2  45366  sprsymrelf1lem  46159  sprsymrelfolem2  46161  prmdvdsfmtnof  46254  prmdvdsfmtnof1  46255  perfectALTV  46391  tgoldbach  46485  uspgrsprf  46524  pzriprnglem4  46808  2zlidl  46832  2zrngamgm  46837  ply1mulgsumlem1  47067  ply1mulgsumlem2  47068  lincsumcl  47112  lincscmcl  47113  ellcoellss  47116  sepfsepc  47560  seppcld  47562