Theorem inv1 4349

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 4188	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3958	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3960	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4191	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3952	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3436   ∩ cin 3902

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 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  undif1  4427  dfif4  4492  rint0  4938  iinrab2  5019  riin0  5031  xpriindi  5779  xpssres  5969  resdmdfsn  5982  elrid  5997  imainrect  6130  xpima  6131  cnvrescnv  6144  dmresv  6149  curry1  8037  curry2  8040  fpar  8049  oev2  8441  hashresfn  14247  dmhashres  14248  gsumxp  19855  pjpm  21615  ptbasfi  23466  mbfmcst  34227  0rrv  34419  vonf1owev  35081  pol0N  39888