| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexlimivw | Structured version Visualization version GIF version | ||
| Description: Weaker version of rexlimiv 3148. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.) |
| Ref | Expression |
|---|---|
| rexlimivw.1 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| rexlimivw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexlimivw.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | adantl 481 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) |
| 3 | 2 | rexlimiva 3147 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ 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-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: r19.36v 3184 r19.45v 3193 r19.44v 3194 r19.29vvaOLD 3217 sbcreu 3876 eliun 4995 reusv3i 5404 elrnmptg 5972 fvelrnb 6969 fvelimab 6981 iinpreima 7089 fmpt 7130 fliftfun 7332 elrnmpo 7569 ovelrn 7609 onuninsuci 7861 fiunlem 7966 releldm2 8068 poxp2 8168 poxp3 8175 orderseqlem 8182 tfrlem4 8419 naddunif 8731 iiner 8829 elixpsn 8977 isfi 9016 card2on 9594 brttrcl 9753 tz9.12lem1 9827 rankwflemb 9833 rankxpsuc 9922 scott0 9926 isnum2 9985 cardiun 10022 cardalephex 10130 dfac5lem4 10166 dfac5lem4OLD 10168 dfac12k 10188 cflim2 10303 cfss 10305 cfslb2n 10308 enfin2i 10361 fin23lem30 10382 itunitc 10461 axdc3lem2 10491 iundom2g 10580 pwcfsdom 10623 cfpwsdom 10624 tskr1om2 10808 genpelv 11040 prlem934 11073 suplem1pr 11092 supexpr 11094 supsrlem 11151 supsr 11152 fimaxre3 12214 iswrd 14554 caurcvgr 15710 caurcvg 15713 caucvg 15715 vdwapval 17011 restsspw 17476 mreunirn 17644 brssc 17858 arwhoma 18090 gexcl3 19605 dvdsr 20362 rhmdvdsr 20508 ellspsn 21001 lspprel 21093 ellspd 21822 iincld 23047 ssnei 23118 neindisj2 23131 neitr 23188 lecldbas 23227 tgcnp 23261 cncnp2 23289 lmmo 23388 is2ndc 23454 fbfinnfr 23849 fbunfip 23877 filunirn 23890 fbflim2 23985 flimcls 23993 hauspwpwf1 23995 flftg 24004 isfcls 24017 fclsbas 24029 isfcf 24042 ustfilxp 24221 ustbas 24236 restutop 24246 ucnima 24290 xmetunirn 24347 metss 24521 metrest 24537 restmetu 24583 qdensere 24790 elpi1 25078 lmmbr 25292 caun0 25315 nulmbl2 25571 itg2l 25764 aannenlem2 26371 taylfval 26400 ulmcl 26424 ulmpm 26426 ulmss 26440 elno 27690 nofun 27694 norn 27696 madeval2 27892 elmade 27906 tglnunirn 28556 ishpg 28767 edglnl 29160 uhgrwkspthlem1 29773 usgr2pth 29784 umgr2wlk 29969 elwwlks2ons3 29975 clwwlknun 30131 frgrncvvdeqlem3 30320 frgr2wwlkn0 30347 frgrreg 30413 hhcms 31222 hhsscms 31297 occllem 31322 occl 31323 chscllem2 31657 r19.29ffa 32490 rabfmpunirn 32663 kerunit 33349 tpr2rico 33911 gsumesum 34060 esumcst 34064 esumfsup 34071 esumpcvgval 34079 esumcvg 34087 sigaclcuni 34119 mbfmfun 34254 dya2icoseg2 34280 bnj66 34874 bnj517 34899 cusgr3cyclex 35141 rellysconn 35256 cvmliftlem15 35303 satffunlem2lem1 35409 r1peuqusdeg1 35648 dfrdg4 35952 brcolinear2 36059 brcolinear 36060 ellines 36153 poimirlem29 37656 volsupnfl 37672 unirep 37721 filbcmb 37747 islshpkrN 39121 ispointN 39744 pmapglbx 39771 rngunsnply 43181 elsetpreimafvbi 47378 grtrif1o 47909 |
| Copyright terms: Public domain | W3C validator |