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 3009. (Contributed by FL, 19-Sep-2011.) |
Ref | Expression |
---|---|
rexlimivw.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
rexlimivw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivw.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | rexlimiv 3009 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: r19.29vva 3062 r19.36v 3066 r19.44v 3075 r19.45v 3076 sbcreu 3482 eliun 4460 reusv3i 4801 elrnmptg 5296 fvelrnb 6153 fvelimab 6163 iinpreima 6253 fmpt 6289 fliftfun 6462 elrnmpt2 6671 ovelrn 6708 onuninsuci 6932 fun11iun 7019 releldm2 7109 tfrlem4 7362 iiner 7706 elixpsn 7833 isfi 7865 card2on 8342 tz9.12lem1 8533 rankwflemb 8539 rankxpsuc 8628 scott0 8632 isnum2 8654 cardiun 8691 cardalephex 8796 dfac5lem4 8832 dfac12k 8852 cflim2 8968 cfss 8970 cfslb2n 8973 enfin2i 9026 fin23lem30 9047 itunitc 9126 axdc3lem2 9156 iundom2g 9241 pwcfsdom 9284 cfpwsdom 9285 tskr1om2 9469 genpelv 9701 prlem934 9734 suplem1pr 9753 supexpr 9755 supsrlem 9811 supsr 9812 fimaxre3 10849 iswrd 13162 caurcvgr 14252 caurcvg 14255 caucvg 14257 vdwapval 15515 restsspw 15915 mreunirn 16084 brssc 16297 arwhoma 16518 gexcl3 17825 dvdsr 18469 lspsnel 18824 lspprel 18915 ellspd 19960 iincld 20653 ssnei 20724 neindisj2 20737 neitr 20794 lecldbas 20833 tgcnp 20867 cncnp2 20895 lmmo 20994 is2ndc 21059 fbfinnfr 21455 fbunfip 21483 filunirn 21496 fbflim2 21591 flimcls 21599 hauspwpwf1 21601 flftg 21610 isfcls 21623 fclsbas 21635 isfcf 21648 ustfilxp 21826 ustbas 21841 restutop 21851 ucnima 21895 xmetunirn 21952 metss 22123 metrest 22139 restmetu 22185 qdensere 22383 elpi1 22653 lmmbr 22864 caun0 22887 nulmbl2 23111 itg2l 23302 aannenlem2 23888 taylfval 23917 ulmcl 23939 ulmpm 23941 ulmss 23955 tglnunirn 25243 ishpg 25451 3v3e3cycl1 26172 iseupa 26492 frgrancvvdeqlem4 26560 frg2wotn0 26583 usgreghash2spot 26596 numclwwlkun 26606 hhcms 27444 hhsscms 27520 occllem 27546 occl 27547 chscllem2 27881 rabfmpunirn 28833 rhmdvdsr 29149 kerunit 29154 tpr2rico 29286 gsumesum 29448 esumcst 29452 esumfsup 29459 esumpcvgval 29467 esumcvg 29475 sigaclcuni 29508 mbfmfun 29643 dya2icoseg2 29667 bnj66 30184 bnj517 30209 rellyscon 30487 cvmliftlem15 30534 orderseqlem 30993 nofun 31046 norn 31048 dfrdg4 31228 brcolinear2 31335 brcolinear 31336 ellines 31429 poimirlem29 32608 volsupnfl 32624 unirep 32677 filbcmb 32705 islshpkrN 33425 ispointN 34046 pmapglbx 34073 rngunsnply 36762 uhgr1wlkspthlem1 40959 usgr2pth 40970 umgr2wlk 41156 frgrncvvdeqlem4 41472 frgr2wwlkn0 41493 fusgreg2wsp 41500 fusgreghash2wsp 41502 av-frgrareg 41548 |
Copyright terms: Public domain | W3C validator |