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 3960	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3962	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4192	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3954	1 ⊢ (𝐴 ∩ V) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3457   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923

This theorem is used by:  vvin  4366  undif1  4437  dfif4  4505  rint0  4955  iinrab2  5036  riin0  5050  xpriindi  5824  xpssres  6019  resdmdfsn  6033  resdmdfsnOLD  6034  elrid  6050  imainrect  6181  xpima  6182  cnvrescnv  6196  dmresv  6201  imadifssran  6204  curry1  8105  curry2  8108  fpar  8117  oev2  8514  hashresfn  14394  dmhashres  14395  gsumxp  20090  pjpm  21908  ptbasfi  23789  mbfmcst  34714  0rrv  34906  inv2  35532  fineqvomon  35588  vonf1wev  35649  vonf1owevOLD  35651  ecqmap  39156  pol0N  40741