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 3597 | . . 3 | |
2 | 1 | anim1d 588 | . 2 |
3 | 2 | reximdv2 3014 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 wrex 2913 wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-rex 2918 df-in 3581 df-ss 3588 |
This theorem is referenced by: ssn0rex 3936 iunss1 4532 onfr 5763 moriotass 6640 frxp 7287 frfi 8205 fisupcl 8375 supgtoreq 8376 brwdom3 8487 unwdomg 8489 tcrank 8747 hsmexlem2 9249 pwfseqlem3 9482 grur1 9642 suplem1pr 9874 fimaxre2 10969 suprfinzcl 11492 lbzbi 11776 suprzub 11779 uzsupss 11780 zmin 11784 ssnn0fi 12784 elss2prb 13269 scshwfzeqfzo 13572 rexico 14093 rlim3 14229 rlimclim 14277 caurcvgr 14404 alzdvds 15042 bitsfzolem 15156 pclem 15543 0ram2 15725 0ramcl 15727 symgextfo 17842 lsmless1x 18059 lsmless2x 18060 dprdss 18428 ablfac2 18488 subrgdvds 18794 ssrest 20980 locfincf 21334 fbun 21644 fgss 21677 isucn2 22083 metust 22363 psmetutop 22372 lebnumlem3 22762 lebnum 22763 cfil3i 23067 cfilss 23068 fgcfil 23069 iscau4 23077 ivthle 23225 ivthle2 23226 lhop1lem 23776 lhop2 23778 ply1divex 23896 plyss 23955 dgrlem 23985 elqaa 24077 aannenlem2 24084 reeff1olem 24200 rlimcnp 24692 ftalem3 24801 pntlem3 25298 tgisline 25522 axcontlem2 25845 frgrwopreg1 27182 frgrwopreg2 27183 shless 28218 xlt2addrd 29523 ssnnssfz 29549 xreceu 29630 archirngz 29743 archiabllem1b 29746 locfinreflem 29907 crefss 29916 esumpcvgval 30140 sigaclci 30195 eulerpartlemgvv 30438 eulerpartlemgh 30440 signsply0 30628 iccllysconn 31232 frmin 31739 fgmin 32365 knoppndvlem18 32520 poimirlem26 33435 poimirlem30 33439 volsupnfl 33454 cover2 33508 filbcmb 33535 istotbnd3 33570 sstotbnd 33574 heibor1lem 33608 isdrngo2 33757 isdrngo3 33758 qsss1 34053 islsati 34281 paddss1 35103 paddss2 35104 hdmap14lem2a 37159 pellfundre 37445 pellfundge 37446 pellfundglb 37449 hbtlem3 37697 hbtlem5 37698 itgoss 37733 radcnvrat 38513 fiminre2 39594 uzubico 39795 uzubico2 39797 climleltrp 39908 fourierdlem20 40344 smflimlem2 40980 iccelpart 41369 fmtnofac2 41481 ssnn0ssfz 42127 pgrpgt2nabl 42147 |
Copyright terms: Public domain | W3C validator |