Theorem inv1 4355

Description: The intersection of a class with the universal class is itself. Dual of un0 4351. 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 4189	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3959	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3961	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4192	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3953	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1570  Vcvv 3455   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922

This theorem is referenced by:  vvin  4366  undif1  4437  dfif4  4503  rint0  4953  iinrab2  5034  riin0  5048  xpriindi  5822  xpssres  6017  resdmdfsn  6031  resdmdfsnOLD  6032  elrid  6048  imainrect  6179  xpima  6180  cnvrescnv  6194  dmresv  6199  imadifssran  6202  curry1  8095  curry2  8098  fpar  8107  oev2  8504  hashresfn  14372  dmhashres  14373  gsumxp  20041  pjpm  21858  ptbasfi  23738  mbfmcst  34649  0rrv  34841  inv2  35467  fineqvomon  35531  vonf1wev  35592  vonf1owevOLD  35594  ecqmap  39098  pol0N  40683