Theorem inv1 4352

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	⊢ (𝐴 ∩ V) = 𝐴

Proof of Theorem inv1

Step	Hyp	Ref	Expression
1		inss1 4191	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3958	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3960	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4194	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3952	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1542  Vcvv 3442   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  undif1  4430  dfif4  4497  rint0  4945  iinrab2  5027  riin0  5039  xpriindi  5793  xpssres  5985  resdmdfsn  5998  elrid  6013  imainrect  6147  xpima  6148  cnvrescnv  6161  dmresv  6166  curry1  8056  curry2  8059  fpar  8068  oev2  8460  hashresfn  14275  dmhashres  14276  gsumxp  19917  pjpm  21675  ptbasfi  23537  mbfmcst  34437  0rrv  34629  fineqvomon  35296  vonf1owev  35324  ecqmap  38700  pol0N  40285