![]() |
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 4058 | . 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴 | |
2 | ssid 3849 | . . 3 ⊢ 𝐴 ⊆ 𝐴 | |
3 | ssv 3851 | . . 3 ⊢ 𝐴 ⊆ V | |
4 | 2, 3 | ssini 4061 | . 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V) |
5 | 1, 4 | eqssi 3844 | 1 ⊢ (𝐴 ∩ V) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 Vcvv 3415 ∩ cin 3798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-v 3417 df-in 3806 df-ss 3813 |
This theorem is referenced by: undif1 4267 dfif4 4322 rint0 4738 iinrab2 4804 riin0 4815 xpriindi 5492 xpssres 5670 resdmdfsn 5683 elrid 5695 imainrect 5817 xpima 5818 dmresv 5835 curry1 7534 curry2 7537 fpar 7546 oev2 7871 hashresfn 13421 dmhashres 13422 gsumxp 18729 pjpm 20416 ptbasfi 21756 mbfmcst 30867 0rrv 31060 pol0N 35985 |
Copyright terms: Public domain | W3C validator |