Theorem inv1 4330

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 4164	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3944	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3946	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4167	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3938	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1539  Vcvv 3427   ∩ cin 3887

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 2109  ax-9 2117  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3429  df-in 3895  df-ss 3905

This theorem is referenced by:  undif1  4411  dfif4  4476  rint0  4923  iinrab2  5000  riin0  5012  xpriindi  5739  xpssres  5922  resdmdfsn  5935  elrid  5947  imainrect  6078  xpima  6079  cnvrescnv  6092  dmresv  6097  curry1  7920  curry2  7923  fpar  7932  oev2  8320  hashresfn  13998  dmhashres  13999  gsumxp  19521  pjpm  20859  ptbasfi  22676  mbfmcst  32168  0rrv  32360  pol0N  37892