Theorem inv1 3786

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

Step	Hyp	Ref	Expression
1		inss1 3679	. 2 |- ( A i^i _V ) C_ A
2		ssid 3480	. . 3 |- A C_ A
3		ssv 3481	. . 3 |- A C_ _V
4	2, 3	ssini 3682	. 2 |- A C_ ( A i^i _V )
5	1, 4	eqssi 3477	1 |- ( A i^i _V ) = A

Syntax hints:   = wceq 1437   _Vcvv 3078   i^i cin 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-ss 3447

This theorem is referenced by:  undif1  3867  dfif4  3921  rint0  4290  iinrab2  4356  riin0  4367  xpriindi  4982  xpssres  5150  resdmdfsn  5161  imainrect  5289  xpima  5290  dmresv  5305  curry1  6890  curry2  6893  fpar  6902  oev2  7224  hashresfn  12509  dmhashres  12510  gsumxp  17536  pjpm  19195  ptbasfi  20520  mbfmcst  28946  0rrv  29136  pol0N  33212  xpheOLD  36047