Theorem inv1 4348

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

Syntax hints:   = wceq 1541  Vcvv 3438   ∩ cin 3898

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ss 3916

This theorem is referenced by:  undif1  4426  dfif4  4493  rint0  4941  iinrab2  5023  riin0  5035  xpriindi  5783  xpssres  5975  resdmdfsn  5988  elrid  6003  imainrect  6137  xpima  6138  cnvrescnv  6151  dmresv  6156  curry1  8044  curry2  8047  fpar  8056  oev2  8448  hashresfn  14261  dmhashres  14262  gsumxp  19903  pjpm  21661  ptbasfi  23523  mbfmcst  34365  0rrv  34557  fineqvomon  35223  vonf1owev  35251  pol0N  40108