![]() |
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 3164 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imim1d 75 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralimdv2 2560 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-ral 2473 df-in 3150 df-ss 3157 |
This theorem is referenced by: iinss1 3913 poss 4316 sess2 4356 trssord 4398 funco 5275 funimaexglem 5318 isores3 5837 isoini2 5841 smores 6317 smores2 6319 tfrlem5 6339 resixp 6759 ac6sfi 6926 difinfinf 7130 peano5nnnn 7921 peano5nni 8952 caucvgre 11022 rexanuz 11029 cau3lem 11155 isumclim3 11463 fsumiun 11517 pcfac 12382 ctinf 12481 strsetsid 12545 imasaddfnlemg 12791 tgcn 14165 tgcnp 14166 cnss2 14184 cncnp 14187 sslm 14204 metrest 14463 rescncf 14525 suplociccex 14560 limcresi 14592 nninfsellemeq 15222 |
Copyright terms: Public domain | W3C validator |