Theorem inv1 4302

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 4155	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3937	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3939	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4158	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3931	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1538  Vcvv 3441   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  undif1  4382  dfif4  4440  rint0  4878  iinrab2  4955  riin0  4967  xpriindi  5671  xpssres  5855  resdmdfsn  5868  elrid  5880  imainrect  6005  xpima  6006  cnvrescnv  6019  dmresv  6024  curry1  7782  curry2  7785  fpar  7794  oev2  8131  hashresfn  13696  dmhashres  13697  gsumxp  19089  pjpm  20397  ptbasfi  22186  mbfmcst  31627  0rrv  31819  pol0N  37205