New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ssel | GIF version |
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssel | ⊢ (A ⊆ B → (C ∈ A → C ∈ B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3262 | . . . . . 6 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B)) | |
2 | 1 | biimpi 186 | . . . . 5 ⊢ (A ⊆ B → ∀x(x ∈ A → x ∈ B)) |
3 | 2 | 19.21bi 1758 | . . . 4 ⊢ (A ⊆ B → (x ∈ A → x ∈ B)) |
4 | 3 | anim2d 548 | . . 3 ⊢ (A ⊆ B → ((x = C ∧ x ∈ A) → (x = C ∧ x ∈ B))) |
5 | 4 | eximdv 1622 | . 2 ⊢ (A ⊆ B → (∃x(x = C ∧ x ∈ A) → ∃x(x = C ∧ x ∈ B))) |
6 | df-clel 2349 | . 2 ⊢ (C ∈ A ↔ ∃x(x = C ∧ x ∈ A)) | |
7 | df-clel 2349 | . 2 ⊢ (C ∈ B ↔ ∃x(x = C ∧ x ∈ B)) | |
8 | 5, 6, 7 | 3imtr4g 261 | 1 ⊢ (A ⊆ B → (C ∈ A → C ∈ B)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 ⊆ wss 3257 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-ss 3259 |
This theorem is referenced by: ssel2 3268 sseli 3269 sseld 3272 sstr2 3279 ssralv 3330 ssrexv 3331 ralss 3332 rexss 3333 ssconb 3399 sscon 3400 ssdif 3401 unss1 3432 ssrin 3480 difin2 3516 reuss2 3535 reupick 3539 sssn 3864 uniss 3912 ss2iun 3984 ssiun 4008 iinss 4017 ssofss 4076 unipw 4117 sspwb 4118 pwadjoin 4119 eqpw1uni 4330 ssopab2b 4713 ssrel 4844 xpss12 4855 cnvss 4885 dmss 4906 dmcosseq 4973 ssreseq 4997 iss 5000 resopab2 5001 ssrnres 5059 dfco2a 5081 cores 5084 funssres 5144 fununi 5160 funimass3 5404 funfvima2 5460 f1elima 5474 resoprab2 5582 clos1conn 5879 |
Copyright terms: Public domain | W3C validator |