MPE Home 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  |-  ( A  i^i  _V )  =  A

Proof of Theorem inv1
StepHypRef Expression
1 inss1 3296 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3118 . . 3  |-  A  C_  A
3 ssv 3119 . . 3  |-  A  C_  _V
42, 3ssini 3299 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3116 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619   _Vcvv 2727    i^i 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