Theorem inv1 4345

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 4184	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3952	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3954	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4187	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3946	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1541  Vcvv 3436   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  undif1  4423  dfif4  4488  rint0  4936  iinrab2  5016  riin0  5028  xpriindi  5775  xpssres  5966  resdmdfsn  5979  elrid  5994  imainrect  6128  xpima  6129  cnvrescnv  6142  dmresv  6147  curry1  8034  curry2  8037  fpar  8046  oev2  8438  hashresfn  14247  dmhashres  14248  gsumxp  19888  pjpm  21645  ptbasfi  23496  mbfmcst  34272  0rrv  34464  fineqvomon  35134  vonf1owev  35152  pol0N  39956