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

Theorem inv1 3481
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 3389 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3197 . . 3  |-  A  C_  A
3 ssv 3198 . . 3  |-  A  C_  _V
42, 3ssini 3392 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3195 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623   _Vcvv 2788    i^i cin 3151
This theorem is referenced by:  undif1  3529  dfif4  3576  rint0  3902  iinrab2  3965  riin0  3975  xpriindi  4822  xpssres  4989  imainrect  5119  dmresv  5132  curry1  6210  curry2  6213  fpar  6222  oev2  6522  gsumxp  15227  pjpm  16608  ptbasfi  17276  hashresfn  23173  dmhashres  23174  xpima  23202  mbfmcst  23564  0rrv  23654  domrancur1b  25200  domrancur1c  25202  selsubf3  25991  pol0N  30098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator