Theorem inv1 3922

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 3795	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3587	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3588	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 3798	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3584	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1475  Vcvv 3173   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  undif1  3995  dfif4  4051  rint0  4452  iinrab2  4519  riin0  4530  xpriindi  5180  xpssres  5354  resdmdfsn  5365  imainrect  5494  xpima  5495  dmresv  5511  curry1  7156  curry2  7159  fpar  7168  oev2  7490  hashresfn  12990  dmhashres  12991  gsumxp  18198  pjpm  19871  ptbasfi  21194  mbfmcst  29648  0rrv  29840  pol0N  34213