Theorem inv1 4397

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 4236	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 4005	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 4007	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4239	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3999	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1539  Vcvv 3479   ∩ cin 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-ss 3967

This theorem is referenced by:  undif1  4475  dfif4  4540  rint0  4987  iinrab2  5069  riin0  5081  xpriindi  5846  xpssres  6035  resdmdfsn  6048  elrid  6063  imainrect  6200  xpima  6201  cnvrescnv  6214  dmresv  6219  curry1  8130  curry2  8133  fpar  8142  oev2  8562  hashresfn  14380  dmhashres  14381  gsumxp  19995  pjpm  21729  ptbasfi  23590  mbfmcst  34262  0rrv  34454  pol0N  39912