Theorem inv1 4339

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 4178	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3945	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3947	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4181	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3939	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1542  Vcvv 3430   ∩ cin 3889

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  undif1  4417  dfif4  4483  rint0  4931  iinrab2  5013  riin0  5025  xpriindi  5783  xpssres  5975  resdmdfsn  5988  elrid  6003  imainrect  6137  xpima  6138  cnvrescnv  6151  dmresv  6156  curry1  8045  curry2  8048  fpar  8057  oev2  8449  hashresfn  14264  dmhashres  14265  gsumxp  19909  pjpm  21665  ptbasfi  23524  mbfmcst  34409  0rrv  34601  fineqvomon  35268  vonf1owev  35296  ecqmap  38761  pol0N  40346