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 3833 | . 2 | |
2 | ssid 3624 | . . 3 | |
3 | ssv 3625 | . . 3 | |
4 | 2, 3 | ssini 3836 | . 2 |
5 | 1, 4 | eqssi 3619 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 cvv 3200 cin 3573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 |
This theorem is referenced by: undif1 4043 dfif4 4101 rint0 4517 iinrab2 4583 riin0 4594 xpriindi 5258 xpssres 5434 resdmdfsn 5445 imainrect 5575 xpima 5576 dmresv 5593 curry1 7269 curry2 7272 fpar 7281 oev2 7603 hashresfn 13128 dmhashres 13129 gsumxp 18375 pjpm 20052 ptbasfi 21384 mbfmcst 30321 0rrv 30513 pol0N 35195 |
Copyright terms: Public domain | W3C validator |