Theorem inv1 4378

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 4217	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3986	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3988	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4220	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3980	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3464   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-ss 3948

This theorem is referenced by:  undif1  4456  dfif4  4521  rint0  4969  iinrab2  5051  riin0  5063  xpriindi  5821  xpssres  6010  resdmdfsn  6023  elrid  6038  imainrect  6175  xpima  6176  cnvrescnv  6189  dmresv  6194  curry1  8108  curry2  8111  fpar  8120  oev2  8540  hashresfn  14363  dmhashres  14364  gsumxp  19962  pjpm  21673  ptbasfi  23524  mbfmcst  34296  0rrv  34488  pol0N  39933