Theorem inv1 4393

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 4227	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 4003	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 4005	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4230	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3997	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1541  Vcvv 3474   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  undif1  4474  dfif4  4542  rint0  4993  iinrab2  5072  riin0  5084  xpriindi  5834  xpssres  6016  resdmdfsn  6029  elrid  6043  imainrect  6177  xpima  6178  cnvrescnv  6191  dmresv  6196  curry1  8086  curry2  8089  fpar  8098  oev2  8519  hashresfn  14296  dmhashres  14297  gsumxp  19838  pjpm  21254  ptbasfi  23076  mbfmcst  33246  0rrv  33438  pol0N  38768