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

Step	Hyp	Ref	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
4	2, 3	ssini 3594	. 2 |- A C_ ( A i^i _V )
5	1, 4	eqssi 3393	1 |- ( A i^i _V ) = A

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