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

Theorem inv1 3483
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 3391 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3199 . . 3  |-  A  C_  A
3 ssv 3200 . . 3  |-  A  C_  _V
42, 3ssini 3394 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3197 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1624   _Vcvv 2790    i^i cin 3153
This theorem is referenced by:  undif1  3531  dfif4  3578  rint0  3904  iinrab2  3967  riin0  3977  xpriindi  4822  xpssres  4989  imainrect  5119  dmresv  5131  curry1  6172  curry2  6175  fpar  6184  oev2  6518  gsumxp  15222  pjpm  16603  ptbasfi  17271  domrancur1b  24600  domrancur1c  24602  selsubf3  25391  pol0N  29366
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator