![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssriv | GIF version |
Description: Inference rule based on subclass definition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssriv.1 | ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) |
Ref | Expression |
---|---|
ssriv | ⊢ 𝐴 ⊆ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 2989 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | ssriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1383 | 1 ⊢ 𝐴 ⊆ 𝐵 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ⊆ wss 2974 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-in 2980 df-ss 2987 |
This theorem is referenced by: ssid 3019 ssv 3020 difss 3099 ssun1 3136 inss1 3193 unssdif 3206 inssdif 3207 unssin 3210 inssun 3211 difindiss 3225 undif3ss 3232 0ss 3289 difprsnss 3532 snsspw 3564 pwprss 3605 pwtpss 3606 uniin 3629 iuniin 3696 iundif2ss 3751 iunpwss 3772 pwuni 3971 pwunss 4046 omsson 4361 limom 4362 xpsspw 4478 dmin 4571 dmrnssfld 4623 dmcoss 4629 dminss 4768 imainss 4769 dmxpss 4783 rnxpid 4785 enq0enq 6683 nqnq0pi 6690 nqnq0 6693 zssre 8439 zsscn 8440 nnssz 8449 uzssz 8719 divfnzn 8787 zssq 8793 qssre 8796 rpssre 8825 ixxssxr 8999 ixxssixx 9001 iooval2 9014 ioossre 9034 rge0ssre 9076 fzssuz 9159 fzssp1 9161 uzdisj 9186 nn0disj 9225 fzossfz 9251 fzouzsplit 9265 fzossnn 9275 fzo0ssnn0 9301 fclim 10271 infssuzcldc 10491 prmssnn 10638 bj-omsson 10915 |
Copyright terms: Public domain | W3C validator |