Theorem inv1 4328

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 4162	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3943	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3945	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4165	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3937	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1539  Vcvv 3432   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  undif1  4409  dfif4  4474  rint0  4921  iinrab2  4999  riin0  5011  xpriindi  5745  xpssres  5928  resdmdfsn  5941  elrid  5953  imainrect  6084  xpima  6085  cnvrescnv  6098  dmresv  6103  curry1  7944  curry2  7947  fpar  7956  oev2  8353  hashresfn  14054  dmhashres  14055  gsumxp  19577  pjpm  20915  ptbasfi  22732  mbfmcst  32226  0rrv  32418  pol0N  37923