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

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

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