Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssralv | Unicode version |
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
Ref | Expression |
---|---|
ssralv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3086 | . . 3 | |
2 | 1 | imim1d 75 | . 2 |
3 | 2 | ralimdv2 2500 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 wral 2414 wss 3066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-ral 2419 df-in 3072 df-ss 3079 |
This theorem is referenced by: iinss1 3820 poss 4215 sess2 4255 trssord 4297 funco 5158 funimaexglem 5201 isores3 5709 isoini2 5713 smores 6182 smores2 6184 tfrlem5 6204 resixp 6620 ac6sfi 6785 difinfinf 6979 peano5nnnn 7693 peano5nni 8716 caucvgre 10746 rexanuz 10753 cau3lem 10879 isumclim3 11185 fsumiun 11239 ctinf 11932 strsetsid 11981 tgcn 12366 tgcnp 12367 cnss2 12385 cncnp 12388 sslm 12405 metrest 12664 rescncf 12726 suplociccex 12761 limcresi 12793 nninfsellemeq 13199 |
Copyright terms: Public domain | W3C validator |