Theorem inv1 4357

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 4196	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3966	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3968	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4199	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3960	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3444   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  undif1  4435  dfif4  4500  rint0  4948  iinrab2  5029  riin0  5041  xpriindi  5790  xpssres  5978  resdmdfsn  5991  elrid  6006  imainrect  6142  xpima  6143  cnvrescnv  6156  dmresv  6161  curry1  8060  curry2  8063  fpar  8072  oev2  8464  hashresfn  14281  dmhashres  14282  gsumxp  19882  pjpm  21593  ptbasfi  23444  mbfmcst  34223  0rrv  34415  vonf1owev  35068  pol0N  39876