![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssel | GIF version |
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssel | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3028 | . . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | biimpi 119 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | 19.21bi 1502 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | anim2d 331 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
5 | 4 | eximdv 1815 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
6 | df-clel 2091 | . 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴)) | |
7 | df-clel 2091 | . 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)) | |
8 | 5, 6, 7 | 3imtr4g 204 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∀wal 1294 = wceq 1296 ∃wex 1433 ∈ wcel 1445 ⊆ 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-in 3019 df-ss 3026 |
This theorem is referenced by: ssel2 3034 sseli 3035 sseld 3038 sstr2 3046 ssralv 3100 ssrexv 3101 ralss 3102 rexss 3103 ssconb 3148 sscon 3149 ssdif 3150 unss1 3184 ssrin 3240 difin2 3277 reuss2 3295 reupick 3299 sssnm 3620 uniss 3696 ss2iun 3767 ssiun 3794 iinss 3803 disjss2 3847 disjss1 3850 pwnss 4015 sspwb 4067 ssopab2b 4127 soss 4165 sucssel 4275 ssorduni 4332 onintonm 4362 onnmin 4412 ssnel 4413 wessep 4421 ssrel 4555 ssrel2 4557 ssrelrel 4567 xpss12 4574 cnvss 4640 dmss 4666 elreldm 4693 dmcosseq 4736 relssres 4783 iss 4791 resopab2 4792 issref 4847 ssrnres 4907 dfco2a 4965 cores 4968 funssres 5090 fununi 5116 funimaexglem 5131 dfimafn 5388 funimass4 5390 funimass3 5454 dff4im 5484 funfvima2 5566 funfvima3 5567 f1elima 5590 riotass2 5672 ssoprab2b 5744 resoprab2 5780 releldm2 5993 reldmtpos 6056 dmtpos 6059 rdgss 6186 ss2ixp 6508 fiintim 6719 negf1o 7957 lbreu 8503 lbinf 8506 eqreznegel 9198 negm 9199 iccsupr 9532 negfi 10790 sumrbdclem 10935 metrest 12308 bdop 12490 bj-nnen2lp 12573 exmidsbthrlem 12633 |
Copyright terms: Public domain | W3C validator |