Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inv1 Unicode version

Theorem inv1 3388
 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.)
Assertion
Ref Expression
inv1

Proof of Theorem inv1
StepHypRef Expression
1 inss1 3296 . 2
2 ssid 3118 . . 3
3 ssv 3119 . . 3
42, 3ssini 3299 . 2
51, 4eqssi 3116 1
 Colors of variables: wff set class Syntax hints:   wceq 1619  cvv 2727   cin 3077 This theorem is referenced by:  undif1  3435  dfif4  3481  rint0  3800  iinrab2  3863  riin0  3873  xpriindi  4729  xpssres  4896  imainrect  5026  dmresv  5038  curry1  6062  curry2  6065  fpar  6074  oev2  6408  gsumxp  15062  pjpm  16440  ptbasfi  17108  domrancur1b  24366  domrancur1c  24368  selsubf3  25157  pol0N  28787 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
 Copyright terms: Public domain W3C validator