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

Theorem inv1 3763
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 3654 . 2  |-  ( A  i^i  _V )  C_  A
2 ssid 3453 . . 3  |-  A  C_  A
3 ssv 3454 . . 3  |-  A  C_  _V
42, 3ssini 3657 . 2  |-  A  C_  ( A  i^i  _V )
51, 4eqssi 3450 1  |-  ( A  i^i  _V )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446   _Vcvv 3047    i^i cin 3405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413  df-ss 3420
This theorem is referenced by:  undif1  3844  dfif4  3898  rint0  4278  iinrab2  4344  riin0  4355  xpriindi  4974  xpssres  5142  resdmdfsn  5153  imainrect  5281  xpima  5282  dmresv  5297  curry1  6893  curry2  6896  fpar  6905  oev2  7230  hashresfn  12530  dmhashres  12531  gsumxp  17620  pjpm  19283  ptbasfi  20608  mbfmcst  29093  0rrv  29296  pol0N  33486  xpheOLD  36389
  Copyright terms: Public domain W3C validator