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

Theorem inv1 3786
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 3679 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3480 . . 3  |-  A  C_  A
3 ssv 3481 . . 3  |-  A  C_  _V
42, 3ssini 3682 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3477 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   _Vcvv 3078    i^i cin 3432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-ss 3447
This theorem is referenced by:  undif1  3867  dfif4  3921  rint0  4290  iinrab2  4356  riin0  4367  xpriindi  4982  xpssres  5150  resdmdfsn  5161  imainrect  5289  xpima  5290  dmresv  5305  curry1  6890  curry2  6893  fpar  6902  oev2  7224  hashresfn  12509  dmhashres  12510  gsumxp  17536  pjpm  19195  ptbasfi  20520  mbfmcst  28946  0rrv  29136  pol0N  33212  xpheOLD  36047
  Copyright terms: Public domain W3C validator