Theorem rexlimiva 3125

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimiv  3126  rexlimivw  3129  rexraleqim  3597  rexopabb  5466  unon  7761  tfrlem16  8312  oawordeulem  8469  nneob  8571  unfi  9080  ominf  9148  unfilem1  9189  fival  9296  elfi2  9298  fi0  9304  fiin  9306  djuss  9813  djuun  9819  updjud  9827  finnum  9841  dif1card  9901  fseqenlem2  9916  dfac8alem  9920  alephfp  9999  cflim2  10154  isfin1-3  10277  fin67  10286  isfin7-2  10287  axdc3lem  10341  axdc3lem2  10342  iunfo  10430  iundom2g  10431  winainflem  10584  rankcf  10668  map2psrpr  11001  supsrlem  11002  1re  11112  0re  11114  00id  11288  addrid  11293  0cnALT  11348  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  18813  smndex1mgm  18815  smndex1mndlem  18817  dfgrp2  18875  pzriprnglem4  21421  psgndiflemA  21538  ppttop  22922  epttop  22924  neips  23028  lmmo  23295  2ndctop  23362  2ndcsep  23374  fbncp  23754  fgcl  23793  filuni  23800  tgioo  24711  zcld  24729  cphsscph  25178  elovolm  25403  nulmbl2  25464  ellimc3  25807  limcflf  25809  pilem3  26390  perfect  27169  2vmadivsum  27479  selberg3lem2  27496  selberg4  27499  pntrsumbnd2  27505  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntpbnd  27526  pnt3  27550  elnoOLD  27585  noreson  27599  nosupbnd1lem5  27651  noinfbnd1lem5  27666  axcontlem12  28953  axcont  28954  clwwlkn1loopb  30023  eleclclwwlkn  30056  uhgr3cyclex  30162  frgrreggt1  30373  norm1exi  31230  nmcexi  32006  lnconi  32013  pjssdif1i  32155  stri  32237  hstri  32245  stcltrthi  32258  shatomici  32338  qsxpid  33327  dispcmp  33872  isrnmeas  34213  dya2iocucvr  34297  sxbrsigalem1  34298  eulerpartlemt  34384  bnj1398  35046  bnj1498  35073  fnrelpredd  35102  r1omfi  35116  wevgblacfn  35153  satfrnmapom  35414  gonar  35439  goalr  35441  satffun  35453  mthmblem  35624  lindsdom  37664  mblfinlem3  37709  ismblfin  37711  volsupnfl  37715  itg2addnclem  37721  itg2addnc  37724  cover2  37765  prtlem16  38978  rexzrexnn0  42907  isnumbasgrplem2  43207  dgraalem  43248  onsucrn  43374  dflim5  43432  dfno2  43531  rp-isfinite5  43620  mnurndlem1  44384  grumnudlem  44388  gruex  44401  islptre  45729  stirlinglem13  46194  stirlinglem14  46195  stirling  46197  etransc  46391  ovolval4lem2  46758  sprsymrelf1lem  47601  sprsymrelfolem2  47603  prmdvdsfmtnof  47696  prmdvdsfmtnof1  47697  perfectALTV  47833  tgoldbach  47927  uspgrsprf  48256  2zlidl  48350  2zrngamgm  48355  ply1mulgsumlem1  48497  ply1mulgsumlem2  48498  lincsumcl  48542  lincscmcl  48543  ellcoellss  48546  sepfsepc  49038  seppcld  49040