![]() |
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 3149. (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 483 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) |
3 | 2 | rexlimiva 3148 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ 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-an 398 df-ex 1783 df-rex 3072 |
This theorem is referenced by: r19.36v 3184 r19.45v 3193 r19.44v 3194 r19.29vvaOLD 3215 sbcreu 3869 eliun 5000 reusv3i 5401 elrnmptg 5956 fvelrnb 6949 fvelimab 6960 iinpreima 7066 fmpt 7105 fliftfun 7304 elrnmpo 7540 ovelrn 7578 onuninsuci 7824 fiunlem 7923 releldm2 8024 poxp2 8124 poxp3 8131 orderseqlem 8138 tfrlem4 8374 naddunif 8688 iiner 8779 elixpsn 8927 isfi 8968 card2on 9545 brttrcl 9704 tz9.12lem1 9778 rankwflemb 9784 rankxpsuc 9873 scott0 9877 isnum2 9936 cardiun 9973 cardalephex 10081 dfac5lem4 10117 dfac12k 10138 cflim2 10254 cfss 10256 cfslb2n 10259 enfin2i 10312 fin23lem30 10333 itunitc 10412 axdc3lem2 10442 iundom2g 10531 pwcfsdom 10574 cfpwsdom 10575 tskr1om2 10759 genpelv 10991 prlem934 11024 suplem1pr 11043 supexpr 11045 supsrlem 11102 supsr 11103 fimaxre3 12156 iswrd 14462 caurcvgr 15616 caurcvg 15619 caucvg 15621 vdwapval 16902 restsspw 17373 mreunirn 17541 brssc 17757 arwhoma 17991 gexcl3 19448 dvdsr 20165 rhmdvdsr 20276 lspsnel 20602 lspprel 20693 ellspd 21341 iincld 22525 ssnei 22596 neindisj2 22609 neitr 22666 lecldbas 22705 tgcnp 22739 cncnp2 22767 lmmo 22866 is2ndc 22932 fbfinnfr 23327 fbunfip 23355 filunirn 23368 fbflim2 23463 flimcls 23471 hauspwpwf1 23473 flftg 23482 isfcls 23495 fclsbas 23507 isfcf 23520 ustfilxp 23699 ustbas 23714 restutop 23724 ucnima 23768 xmetunirn 23825 metss 23999 metrest 24015 restmetu 24061 qdensere 24268 elpi1 24543 lmmbr 24757 caun0 24780 nulmbl2 25035 itg2l 25229 aannenlem2 25824 taylfval 25853 ulmcl 25875 ulmpm 25877 ulmss 25891 nofun 27132 norn 27134 madeval2 27328 elmade 27342 tglnunirn 27779 ishpg 27990 edglnl 28383 uhgrwkspthlem1 28990 usgr2pth 29001 umgr2wlk 29183 elwwlks2ons3 29189 clwwlknun 29345 frgrncvvdeqlem3 29534 frgr2wwlkn0 29561 frgrreg 29627 hhcms 30434 hhsscms 30509 occllem 30534 occl 30535 chscllem2 30869 r19.29ffa 31691 rabfmpunirn 31856 kerunit 32406 tpr2rico 32830 gsumesum 32995 esumcst 32999 esumfsup 33006 esumpcvgval 33014 esumcvg 33022 sigaclcuni 33054 mbfmfun 33189 dya2icoseg2 33215 bnj66 33809 bnj517 33834 cusgr3cyclex 34065 rellysconn 34180 cvmliftlem15 34227 satffunlem2lem1 34333 dfrdg4 34861 brcolinear2 34968 brcolinear 34969 ellines 35062 poimirlem29 36455 volsupnfl 36471 unirep 36520 filbcmb 36546 islshpkrN 37928 ispointN 38551 pmapglbx 38578 rngunsnply 41848 elsetpreimafvbi 45994 |
Copyright terms: Public domain | W3C validator |