![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inv1 | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 3654 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssid 3453 |
. . 3
![]() ![]() ![]() ![]() | |
3 | ssv 3454 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | ssini 3657 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqssi 3450 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 df-in 3413 df-ss 3420 |
This theorem is referenced by: undif1 3844 dfif4 3898 rint0 4278 iinrab2 4344 riin0 4355 xpriindi 4974 xpssres 5142 resdmdfsn 5153 imainrect 5281 xpima 5282 dmresv 5297 curry1 6893 curry2 6896 fpar 6905 oev2 7230 hashresfn 12530 dmhashres 12531 gsumxp 17620 pjpm 19283 ptbasfi 20608 mbfmcst 29093 0rrv 29296 pol0N 33486 xpheOLD 36389 |
Copyright terms: Public domain | W3C validator |