Theorem inv1 4347

Description: The intersection of a class with the universal class is itself. Dual of un0 4343. 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 4132	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3931	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3933	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4135	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3925	1 ⊢ (𝐴 ∩ V) = 𝐴

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3450   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-in 4090

This theorem is used by:  vvin  4358  undif1  4429  dfif4  4497  rint0  4947  iinrab2  5027  riin0  5041  xpriindi  5814  xpssres  6009  resdmdfsn  6023  resdmdfsnOLD  6024  elrid  6040  imainrect  6175  xpima  6176  cnvrescnv  6190  dmresv  6197  imadifssranOLD  6205  curry1  8121  curry2  8124  fpar  8133  oev2  8538  hashresfn  14491  dmhashres  14492  gsumxp  20199  pjpm  22023  ptbasfi  23909  mbfmcst  34941  0rrv  35133  inv2  35761  fineqvomon  35846  vonf1wev  35959  vonf1owevOLD  35961  ecqmap  39490  pol0N  41075