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

Theorem inv1 3685
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 3591 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3396 . . 3  |-  A  C_  A
3 ssv 3397 . . 3  |-  A  C_  _V
42, 3ssini 3594 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3393 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   _Vcvv 2993    i^i cin 3348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363
This theorem is referenced by:  undif1  3775  dfif4  3825  rint0  4189  iinrab2  4254  riin0  4265  xpriindi  4997  xpssres  5165  resdmdfsn  5173  imainrect  5300  xpima  5301  dmresv  5317  curry1  6685  curry2  6688  fpar  6697  oev2  6984  hashresfn  12132  dmhashres  12133  gsumxp  16490  gsumxpOLD  16492  pjpm  18155  ptbasfi  19176  mbfmcst  26696  0rrv  26856  pol0N  33649
  Copyright terms: Public domain W3C validator