Theorem inv1 4421

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 4258	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 4031	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 4033	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4261	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 4025	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1537  Vcvv 3488   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  undif1  4499  dfif4  4563  rint0  5012  iinrab2  5093  riin0  5105  xpriindi  5861  xpssres  6047  resdmdfsn  6060  elrid  6075  imainrect  6212  xpima  6213  cnvrescnv  6226  dmresv  6231  curry1  8145  curry2  8148  fpar  8157  oev2  8579  hashresfn  14389  dmhashres  14390  gsumxp  20018  pjpm  21751  ptbasfi  23610  mbfmcst  34224  0rrv  34416  pol0N  39866