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 3081 | . . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | biimpi 119 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | 19.21bi 1537 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | anim2d 335 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
5 | 4 | eximdv 1852 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
6 | df-clel 2133 | . 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴)) | |
7 | df-clel 2133 | . 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)) | |
8 | 5, 6, 7 | 3imtr4g 204 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∀wal 1329 = wceq 1331 ∃wex 1468 ∈ wcel 1480 ⊆ wss 3066 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 |
This theorem is referenced by: ssel2 3087 sseli 3088 sseld 3091 sstr2 3099 nelss 3153 ssrexf 3154 ssralv 3156 ssrexv 3157 ralss 3158 rexss 3159 ssconb 3204 sscon 3205 ssdif 3206 unss1 3240 ssrin 3296 difin2 3333 reuss2 3351 reupick 3355 sssnm 3676 uniss 3752 ss2iun 3823 ssiun 3850 iinss 3859 disjss2 3904 disjss1 3907 pwnss 4078 sspwb 4133 ssopab2b 4193 soss 4231 sucssel 4341 ssorduni 4398 onintonm 4428 onnmin 4478 ssnel 4479 wessep 4487 ssrel 4622 ssrel2 4624 ssrelrel 4634 xpss12 4641 cnvss 4707 dmss 4733 elreldm 4760 dmcosseq 4805 relssres 4852 iss 4860 resopab2 4861 issref 4916 ssrnres 4976 dfco2a 5034 cores 5037 funssres 5160 fununi 5186 funimaexglem 5201 dfimafn 5463 funimass4 5465 funimass3 5529 dff4im 5559 funfvima2 5643 funfvima3 5644 f1elima 5667 riotass2 5749 ssoprab2b 5821 resoprab2 5861 releldm2 6076 reldmtpos 6143 dmtpos 6146 rdgss 6273 ss2ixp 6598 fiintim 6810 negf1o 8137 lbreu 8696 lbinf 8699 eqreznegel 9399 negm 9400 iccsupr 9742 negfi 10992 sumrbdclem 11138 prodrbdclem 11333 metrest 12664 bdop 13062 bj-nnen2lp 13141 exmidsbthrlem 13206 |
Copyright terms: Public domain | W3C validator |