Theorem inv1 4364

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 4203	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3972	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3974	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4206	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3966	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3450   ∩ cin 3916

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  undif1  4442  dfif4  4507  rint0  4955  iinrab2  5037  riin0  5049  xpriindi  5803  xpssres  5992  resdmdfsn  6005  elrid  6020  imainrect  6157  xpima  6158  cnvrescnv  6171  dmresv  6176  curry1  8086  curry2  8089  fpar  8098  oev2  8490  hashresfn  14312  dmhashres  14313  gsumxp  19913  pjpm  21624  ptbasfi  23475  mbfmcst  34257  0rrv  34449  vonf1owev  35102  pol0N  39910