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 3126 | . . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | biimpi 119 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | 19.21bi 1545 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | anim2d 335 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
5 | 4 | eximdv 1867 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
6 | df-clel 2160 | . 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴)) | |
7 | df-clel 2160 | . 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)) | |
8 | 5, 6, 7 | 3imtr4g 204 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∀wal 1340 = wceq 1342 ∃wex 1479 ∈ wcel 2135 ⊆ wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: ssel2 3132 sseli 3133 sseld 3136 sstr2 3144 nelss 3198 ssrexf 3199 ssralv 3201 ssrexv 3202 ralss 3203 rexss 3204 ssconb 3250 sscon 3251 ssdif 3252 unss1 3286 ssrin 3342 difin2 3379 reuss2 3397 reupick 3401 sssnm 3728 uniss 3804 ss2iun 3875 ssiun 3902 iinss 3911 disjss2 3956 disjss1 3959 pwnss 4132 sspwb 4188 ssopab2b 4248 soss 4286 sucssel 4396 ssorduni 4458 onintonm 4488 onnmin 4539 ssnel 4540 wessep 4549 ssrel 4686 ssrel2 4688 ssrelrel 4698 xpss12 4705 cnvss 4771 dmss 4797 elreldm 4824 dmcosseq 4869 relssres 4916 iss 4924 resopab2 4925 issref 4980 ssrnres 5040 dfco2a 5098 cores 5101 funssres 5224 fununi 5250 funimaexglem 5265 dfimafn 5529 funimass4 5531 funimass3 5595 dff4im 5625 funfvima2 5711 funfvima3 5712 f1elima 5735 riotass2 5818 ssoprab2b 5890 resoprab2 5930 releldm2 6145 reldmtpos 6212 dmtpos 6215 rdgss 6342 ss2ixp 6668 fiintim 6885 negf1o 8271 lbreu 8831 lbinf 8834 eqreznegel 9543 negm 9544 iccsupr 9893 negfi 11155 sumrbdclem 11304 prodrbdclem 11498 fprodmodd 11568 metrest 13053 bdop 13598 bj-nnen2lp 13677 exmidsbthrlem 13742 |
Copyright terms: Public domain | W3C validator |