Theorem rexlimivw 3168

Description: Weaker version of rexlimiv 3165. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)

Hypothesis

Ref	Expression
rexlimivw.1	⊢ (𝜑 → 𝜓)

Assertion

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

Distinct variable group:   𝜓,𝑥

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

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 486	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3164	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  r19.36v  3199  r19.45v  3205  r19.44v  3206  sbcreu  3838  eliun  4964  reusv3i  5376  elrnmptg  5952  fvelrnb  6942  fvelimab  6954  iinpreima  7065  fmpt  7106  fliftfun  7311  elrnmpo  7547  ovelrn  7587  onuninsuci  7835  fiunlem  7938  releldm2  8039  poxp2  8138  poxp3  8145  orderseqlem  8152  tfrlem4  8364  naddunif  8679  iiner  8786  elixpsn  8934  isfi  8971  card2on  9515  brttrcl  9681  tz9.12lem1  9758  rankwflemb  9764  rankxpsuc  9853  scott0  9859  isnum2  9930  cardiun  9967  cardalephex  10073  dfac5lem4  10109  dfac12k  10130  cflim2  10246  cfss  10248  cfslb2n  10251  enfin2i  10304  fin23lem30  10325  itunitc  10404  axdc3lem2  10434  iundom2g  10523  pwcfsdom  10567  cfpwsdom  10568  tskr1om2  10752  genpelv  10984  prlem934  11017  suplem1pr  11036  supexpr  11038  supsrlem  11095  supsr  11096  fimaxre3  12160  iswrd  14551  caurcvgr  15724  caurcvg  15727  caucvg  15729  vdwapval  17032  restsspw  17483  mreunirn  17652  brssc  17870  arwhoma  18101  gexcl3  19656  dvdsr  20443  rhmdvdsr  20590  ellspsn  21101  lspprel  21192  ellspd  21920  iincld  23164  ssnei  23235  neindisj2  23248  neitr  23305  lecldbas  23344  tgcnp  23378  cncnp2  23406  lmmo  23505  is2ndc  23571  fbfinnfr  23966  fbunfip  23994  filunirn  24007  fbflim2  24102  flimcls  24110  hauspwpwf1  24112  flftg  24121  isfcls  24134  fclsbas  24146  isfcf  24159  ustfilxp  24338  ustbas  24352  restutop  24362  ucnima  24405  xmetunirn  24462  metss  24633  metrest  24649  restmetu  24695  qdensere  24894  elpi1  25172  lmmbr  25385  caun0  25408  nulmbl2  25663  itg2l  25856  aannenlem2  26458  taylfval  26487  ulmcl  26509  ulmpm  26511  ulmss  26525  elno  27775  nofun  27778  norn  27780  madeval2  27991  elmade  28015  tglnunirn  28782  ishpg  28999  edglnl  29433  uhgrwkspthlem1  30042  usgr2pth  30053  umgr2wlk  30238  elwwlks2ons3  30244  clwwlknun  30403  frgrncvvdeqlem3  30592  frgr2wwlkn0  30619  frgrreg  30685  hhcms  31495  hhsscms  31570  occllem  31595  occl  31596  chscllem2  31930  r19.29ffa  32758  rabfmpunirn  32938  kerunit  33587  tpr2rico  34246  gsumesum  34393  esumcst  34397  esumfsup  34404  esumpcvgval  34412  esumcvg  34420  sigaclcuni  34452  mbfmfun  34587  dya2icoseg2  34612  bnj66  35192  bnj517  35217  cusgr3cyclex  35526  rellysconn  35641  cvmliftlem15  35688  satffunlem2lem1  35794  r1peuqusdeg1  36033  dfrdg4  36341  brcolinear2  36448  brcolinear  36449  ellines  36542  poimirlem29  38187  volsupnfl  38203  unirep  38252  filbcmb  38278  islshpkrN  39783  ispointN  40405  pmapglbx  40432  rngunsnply  43787  elsetpreimafvbi  48028  cycldlenngric  48581  grtrif1o  48595