| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ssexg | Structured version Visualization version GIF version | ||
| Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
| Ref | Expression |
|---|---|
| ssexg | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sseq2 4010 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
| 2 | 1 | imbi1d 341 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
| 3 | vex 3484 | . . . 4 ⊢ 𝑥 ∈ V | |
| 4 | 3 | ssex 5321 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
| 5 | 2, 4 | vtoclg 3554 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
| 6 | 5 | impcom 407 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 |
| This theorem is referenced by: ssexd 5324 prcssprc 5327 difexg 5329 elpw2g 5333 rabexgOLD 5338 elssabg 5343 abssexg 5382 snexALT 5383 sess1 5650 sess2 5651 riinint 5982 resexg 6045 trsuc 6471 ordsssuc2 6475 mptexg 7241 mptexgf 7242 isofr2 7364 ofres 7716 brrpssg 7745 unexb 7767 unexbOLD 7768 xpexg 7770 abnexg 7776 difex2 7780 uniexr 7783 dmexg 7923 rnexg 7924 resiexg 7934 imaexg 7935 exse2 7939 cnvexg 7946 coexg 7951 fabexgOLD 7961 f1oabexgOLD 7965 resfunexgALT 7972 cofunexg 7973 fnexALT 7975 f1dmex 7981 oprabexd 8000 mpoexxg 8100 suppfnss 8214 tposexg 8265 tz7.48-3 8484 oaabs 8686 erex 8769 mapexOLD 8872 pmvalg 8877 elpmg 8883 elmapssres 8907 pmss12g 8909 ralxpmap 8936 ixpexg 8962 domssl 9038 ssdomg 9040 fiprc 9085 domunsncan 9112 infensuc 9195 pssnn 9208 ssfi 9213 enp1i 9313 unbnn 9332 fodomfi 9350 fodomfiOLD 9370 fival 9452 fiss 9464 dffi3 9471 hartogslem2 9583 card2on 9594 wdomima2g 9626 unxpwdom2 9628 unxpwdom 9629 harwdom 9631 oemapvali 9724 ackbij1lem11 10269 cofsmo 10309 ssfin4 10350 fin23lem11 10357 ssfin2 10360 ssfin3ds 10370 isfin1-3 10426 hsmex3 10474 axdc2lem 10488 ac6num 10519 ttukeylem1 10549 dmct 10564 ondomon 10603 fpwwe2lem3 10673 fpwwe2lem11 10681 fpwwe2lem12 10682 canthwe 10691 wuncss 10785 genpv 11039 genpdm 11042 hashss 14448 wrdexb 14563 shftfval 15109 o1of2 15649 o1rlimmul 15655 isercolllem2 15702 isstruct2 17186 ressval3d 17292 ressabs 17294 prdsbas 17502 fnmrc 17650 mrcfval 17651 isacs1i 17700 mreacs 17701 isssc 17864 ipolerval 18577 ress0g 18775 sylow2a 19637 islbs3 21157 toponsspwpw 22928 basdif0 22960 tgval 22962 eltg 22964 eltg2 22965 tgss 22975 basgen2 22996 2basgen 22997 bastop1 23000 topnex 23003 resttopon 23169 restabs 23173 restcld 23180 restfpw 23187 restcls 23189 restntr 23190 ordtbas2 23199 ordtbas 23200 lmfval 23240 cnrest 23293 cmpcov 23397 cmpsublem 23407 cmpsub 23408 2ndcomap 23466 islocfin 23525 txss12 23613 ptrescn 23647 trfbas2 23851 trfbas 23852 isfildlem 23865 snfbas 23874 trfil1 23894 trfil2 23895 trufil 23918 ssufl 23926 hauspwpwf1 23995 ustval 24211 metrest 24537 cnheibor 24987 metcld2 25341 bcthlem1 25358 mbfimaopn2 25692 0pledm 25708 dvbss 25936 dvreslem 25944 dvres2lem 25945 dvcnp2 25955 dvcnp2OLD 25956 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 dvcnvrelem2 26057 elply2 26235 plyf 26237 plyss 26238 elplyr 26240 plyeq0lem 26249 plyeq0 26250 plyaddlem 26254 plymullem 26255 dgrlem 26268 coeidlem 26276 ulmcn 26442 pserulm 26465 rabexgfGS 32518 abrexdomjm 32526 aciunf1 32673 indval 32838 ress1r 33238 pcmplfin 33859 metidval 33889 sigagenss 34150 measval 34199 omsfval 34296 omssubaddlem 34301 omssubadd 34302 carsggect 34320 erdsze2lem1 35208 erdsze2lem2 35209 cvxpconn 35247 elmsta 35553 dfon2lem3 35786 altxpexg 35979 ivthALT 36336 filnetlem3 36381 bj-sselpwuni 37051 bj-elpwg 37053 bj-restsnss 37084 bj-restsnss2 37085 bj-restb 37095 bj-restuni2 37099 abrexdom 37737 sdclem2 37749 sdclem1 37750 imaexALTV 38331 brssr 38502 sticksstones4 42150 sticksstones14 42161 pssexg 42265 elrfirn 42706 pwssplit4 43101 hbtlem1 43135 hbtlem7 43137 inaex 44316 rabexgf 45029 dvnprodlem2 45962 qndenserrnbllem 46309 sge0ss 46427 psmeasurelem 46485 caragensplit 46515 omeunile 46520 caragenuncl 46528 omeunle 46531 omeiunlempt 46535 carageniuncllem2 46537 fcdmvafv2v 47248 prprval 47501 mpoexxg2 48254 gsumlsscl 48296 lincellss 48343 |
| Copyright terms: Public domain | W3C validator |