![]() |
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 3164 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | imim1d 75 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))) |
3 | 2 | ralimdv2 2560 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ∀wral 2468 ⊆ wss 3144 |
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 6318 smores2 6320 tfrlem5 6340 resixp 6760 ac6sfi 6927 difinfinf 7131 peano5nnnn 7922 peano5nni 8953 caucvgre 11025 rexanuz 11032 cau3lem 11158 isumclim3 11466 fsumiun 11520 pcfac 12385 ctinf 12484 strsetsid 12548 imasaddfnlemg 12794 tgcn 14185 tgcnp 14186 cnss2 14204 cncnp 14207 sslm 14224 metrest 14483 rescncf 14545 suplociccex 14580 limcresi 14612 nninfsellemeq 15242 |
Copyright terms: Public domain | W3C validator |