![]() |
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 3146 | . . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | biimpi 120 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | 19.21bi 1558 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | anim2d 337 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
5 | 4 | eximdv 1880 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
6 | df-clel 2173 | . 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴)) | |
7 | df-clel 2173 | . 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)) | |
8 | 5, 6, 7 | 3imtr4g 205 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∀wal 1351 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ⊆ wss 3131 |
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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3137 df-ss 3144 |
This theorem is referenced by: ssel2 3152 sseli 3153 sseld 3156 sstr2 3164 nelss 3218 ssrexf 3219 ssralv 3221 ssrexv 3222 ralss 3223 rexss 3224 ssconb 3270 sscon 3271 ssdif 3272 unss1 3306 ssrin 3362 difin2 3399 reuss2 3417 reupick 3421 sssnm 3756 uniss 3832 ss2iun 3903 ssiun 3930 iinss 3940 disjss2 3985 disjss1 3988 pwnss 4161 sspwb 4218 ssopab2b 4278 soss 4316 sucssel 4426 ssorduni 4488 onintonm 4518 onnmin 4569 ssnel 4570 wessep 4579 ssrel 4716 ssrel2 4718 ssrelrel 4728 xpss12 4735 cnvss 4802 dmss 4828 elreldm 4855 dmcosseq 4900 relssres 4947 iss 4955 resopab2 4956 issref 5013 ssrnres 5073 dfco2a 5131 cores 5134 funssres 5260 fununi 5286 funimaexglem 5301 dfimafn 5566 funimass4 5568 funimass3 5634 dff4im 5664 funfvima2 5751 funfvima3 5752 f1elima 5776 riotass2 5859 ssoprab2b 5934 resoprab2 5974 releldm2 6188 reldmtpos 6256 dmtpos 6259 rdgss 6386 ss2ixp 6713 fiintim 6930 negf1o 8341 lbreu 8904 lbinf 8907 eqreznegel 9616 negm 9617 iccsupr 9968 negfi 11238 sumrbdclem 11387 prodrbdclem 11581 fprodmodd 11651 mulgpropdg 13030 subgintm 13063 subrgintm 13369 lspsnel6 13499 metrest 14091 bdop 14712 bj-nnen2lp 14791 exmidsbthrlem 14855 |
Copyright terms: Public domain | W3C validator |