![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssrexv | Structured version Visualization version Unicode version |
Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
Ref | Expression |
---|---|
ssrexv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3412 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim1d 574 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | reximdv2 2855 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-rex 2762 df-in 3397 df-ss 3404 |
This theorem is referenced by: iunss1 4281 onfr 5469 moriotass 6298 frxp 6925 frfi 7834 fisupcl 8003 supgtoreq 8004 brwdom3 8115 unwdomg 8117 tcrank 8373 hsmexlem2 8875 pwfseqlem3 9103 grur1 9263 suplem1pr 9495 fimaxre2 10574 suprfinzcl 11073 lbzbi 11275 suprzub 11278 uzsupss 11279 zmin 11283 ssnn0fi 12235 elss2prb 12684 scshwfzeqfzo 12982 rexico 13493 rlim3 13639 rlimclim 13687 caurcvgr 13815 caurcvgrOLD 13816 alzdvds 14432 bitsfzolem 14486 bitsfzolemOLD 14487 pclem 14867 0ram2 15058 0ramcl 15060 symgextfo 17141 lsmless1x 17374 lsmless2x 17375 dprdss 17740 ablfac2 17800 subrgdvds 18100 ssrest 20269 locfincf 20623 fbun 20933 fgss 20966 isucn2 21372 metust 21651 psmetutop 21660 lebnumlem3 22069 lebnumlem3OLD 22072 lebnum 22073 cfil3i 22317 cfilss 22318 fgcfil 22319 iscau4 22327 ivthle 22485 ivthle2 22486 lhop1lem 23044 lhop2 23046 ply1divex 23166 plyss 23232 dgrlem 23262 elqaa 23357 aannenlem2 23364 reeff1olem 23480 rlimcnp 23970 ftalem3 24078 pntlem3 24526 tgisline 24751 axcontlem2 25074 frgrawopreg1 25857 frgrawopreg2 25858 shless 27093 xlt2addrd 28413 ssnnssfz 28442 xreceu 28466 archirngz 28580 archiabllem1b 28583 locfinreflem 28741 crefss 28750 esumpcvgval 28973 sigaclci 29028 eulerpartlemgvv 29282 eulerpartlemgh 29284 signsply0 29512 iccllyscon 30045 frmin 30551 nodenselem4 30644 fgmin 31097 poimirlem26 32030 poimirlem30 32034 volsupnfl 32049 cover2 32104 filbcmb 32131 istotbnd3 32167 sstotbnd 32171 heibor1lem 32205 isdrngo2 32261 isdrngo3 32262 islsati 32631 paddss1 33453 paddss2 33454 hdmap14lem2a 35509 pellfundre 35800 pellfundge 35801 pellfundglb 35804 hbtlem3 36057 hbtlem5 36058 itgoss 36100 radcnvrat 36733 fourierdlem20 38101 iccelpart 38892 ssn0rex 39136 ssnn0ssfz 40638 pgrpgt2nabl 40659 |
Copyright terms: Public domain | W3C validator |