Theorem inv1 4338

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

Syntax hints:   = wceq 1542  Vcvv 3429   ∩ cin 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  undif1  4416  dfif4  4482  rint0  4930  iinrab2  5012  riin0  5024  xpriindi  5791  xpssres  5983  resdmdfsn  5996  elrid  6011  imainrect  6145  xpima  6146  cnvrescnv  6159  dmresv  6164  curry1  8054  curry2  8057  fpar  8066  oev2  8458  hashresfn  14302  dmhashres  14303  gsumxp  19951  pjpm  21688  ptbasfi  23546  mbfmcst  34403  0rrv  34595  fineqvomon  35262  vonf1owev  35290  ecqmap  38770  pol0N  40355