![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssralv | GIF version |
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
Ref | Expression |
---|---|
ssralv | ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3033 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | imim1d 75 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))) |
3 | 2 | ralimdv2 2455 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ∀wral 2370 ⊆ wss 3013 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-ral 2375 df-in 3019 df-ss 3026 |
This theorem is referenced by: iinss1 3764 poss 4149 sess2 4189 trssord 4231 funco 5088 funimaexglem 5131 isores3 5632 isoini2 5636 smores 6095 smores2 6097 tfrlem5 6117 resixp 6530 ac6sfi 6694 peano5nnnn 7524 peano5nni 8523 caucvgre 10545 rexanuz 10552 cau3lem 10678 isumclim3 10982 fsumiun 11036 strsetsid 11692 tgcn 12075 tgcnp 12076 cnss2 12094 cncnp 12097 sslm 12114 metrest 12308 rescncf 12350 nninfsellemeq 12627 |
Copyright terms: Public domain | W3C validator |