Theorem inv1 4350

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 4189	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3956	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3958	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4192	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3950	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1541  Vcvv 3440   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  undif1  4428  dfif4  4495  rint0  4943  iinrab2  5025  riin0  5037  xpriindi  5785  xpssres  5977  resdmdfsn  5990  elrid  6005  imainrect  6139  xpima  6140  cnvrescnv  6153  dmresv  6158  curry1  8046  curry2  8049  fpar  8058  oev2  8450  hashresfn  14263  dmhashres  14264  gsumxp  19905  pjpm  21663  ptbasfi  23525  mbfmcst  34416  0rrv  34608  fineqvomon  35274  vonf1owev  35302  pol0N  40169