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

Theorem inv1 3494
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 3402 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3210 . . 3  |-  A  C_  A
3 ssv 3211 . . 3  |-  A  C_  _V
42, 3ssini 3405 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3208 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632   _Vcvv 2801    i^i cin 3164
This theorem is referenced by:  undif1  3542  dfif4  3589  rint0  3918  iinrab2  3981  riin0  3991  xpriindi  4838  xpssres  5005  imainrect  5135  dmresv  5148  curry1  6226  curry2  6229  fpar  6238  oev2  6538  gsumxp  15243  pjpm  16624  ptbasfi  17292  hashresfn  23189  dmhashres  23190  xpima  23217  mbfmcst  23579  0rrv  23669  domrancur1b  25303  domrancur1c  25305  selsubf3  26094  pol0N  30720
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator