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

Theorem inv1 3442
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 3350 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3158 . . 3  |-  A  C_  A
3 ssv 3159 . . 3  |-  A  C_  _V
42, 3ssini 3353 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3156 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619   _Vcvv 2757    i^i cin 3112
This theorem is referenced by:  undif1  3490  dfif4  3536  rint0  3862  iinrab2  3925  riin0  3935  xpriindi  4796  xpssres  4963  imainrect  5093  dmresv  5105  curry1  6130  curry2  6133  fpar  6142  oev2  6476  gsumxp  15175  pjpm  16556  ptbasfi  17224  domrancur1b  24553  domrancur1c  24555  selsubf3  25344  pol0N  29249
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator