![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > resss | GIF version |
Description: A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
resss | ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 4416 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 3206 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3042 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: Vcvv 2614 ∩ cin 2985 ⊆ wss 2986 × cxp 4402 ↾ cres 4406 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 |
This theorem depends on definitions: df-bi 115 df-tru 1290 df-nf 1393 df-sb 1690 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-v 2616 df-in 2992 df-ss 2999 df-res 4416 |
This theorem is referenced by: relssres 4710 resexg 4712 iss 4718 cocnvres 4912 relresfld 4917 relcoi1 4919 funres 5011 funres11 5042 funcnvres 5043 2elresin 5081 fssres 5138 foimacnv 5222 tposss 5946 dftpos4 5963 smores 5992 smores2 5994 caserel 6699 |
Copyright terms: Public domain | W3C validator |