Theorem inv1 4395

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 4229	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 4005	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 4007	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4232	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3999	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1542  Vcvv 3475   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  undif1  4476  dfif4  4544  rint0  4995  iinrab2  5074  riin0  5086  xpriindi  5837  xpssres  6019  resdmdfsn  6032  elrid  6046  imainrect  6181  xpima  6182  cnvrescnv  6195  dmresv  6200  curry1  8090  curry2  8093  fpar  8102  oev2  8523  hashresfn  14300  dmhashres  14301  gsumxp  19844  pjpm  21263  ptbasfi  23085  mbfmcst  33258  0rrv  33450  pol0N  38780