Theorem inv1 4325

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 4159	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3939	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3941	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4162	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3933	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1539  Vcvv 3422   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  undif1  4406  dfif4  4471  rint0  4918  iinrab2  4995  riin0  5007  xpriindi  5734  xpssres  5917  resdmdfsn  5930  elrid  5942  imainrect  6073  xpima  6074  cnvrescnv  6087  dmresv  6092  curry1  7915  curry2  7918  fpar  7927  oev2  8315  hashresfn  13982  dmhashres  13983  gsumxp  19492  pjpm  20825  ptbasfi  22640  mbfmcst  32126  0rrv  32318  pol0N  37850