![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inv1 | Structured version Visualization version GIF version |
Description: The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
Ref | Expression |
---|---|
inv1 | ⊢ (𝐴 ∩ V) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 4228 | . 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴 | |
2 | ssid 4004 | . . 3 ⊢ 𝐴 ⊆ 𝐴 | |
3 | ssv 4006 | . . 3 ⊢ 𝐴 ⊆ V | |
4 | 2, 3 | ssini 4231 | . 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V) |
5 | 1, 4 | eqssi 3998 | 1 ⊢ (𝐴 ∩ V) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 Vcvv 3473 ∩ cin 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 |
This theorem is referenced by: undif1 4475 dfif4 4543 rint0 4994 iinrab2 5073 riin0 5085 xpriindi 5836 xpssres 6018 resdmdfsn 6031 elrid 6045 imainrect 6180 xpima 6181 cnvrescnv 6194 dmresv 6199 curry1 8094 curry2 8097 fpar 8106 oev2 8527 hashresfn 14305 dmhashres 14306 gsumxp 19886 pjpm 21483 ptbasfi 23306 mbfmcst 33557 0rrv 33749 pol0N 39084 |
Copyright terms: Public domain | W3C validator |