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  5786  xpssres  5978  resdmdfsn  5991  elrid  6006  imainrect  6140  xpima  6141  cnvrescnv  6154  dmresv  6159  curry1  8048  curry2  8051  fpar  8060  oev2  8452  hashresfn  14296  dmhashres  14297  gsumxp  19945  pjpm  21701  ptbasfi  23559  mbfmcst  34422  0rrv  34614  fineqvomon  35281  vonf1owev  35309  ecqmap  38787  pol0N  40372