Theorem inv1 4348

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

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3450   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  vvin  4359  undif1  4430  dfif4  4498  rint0  4948  iinrab2  5028  riin0  5042  xpriindi  5816  xpssres  6011  resdmdfsn  6025  resdmdfsnOLD  6026  elrid  6042  imainrect  6174  xpima  6175  cnvrescnv  6189  dmresv  6194  imadifssran  6197  curry1  8101  curry2  8104  fpar  8113  oev2  8510  hashresfn  14404  dmhashres  14405  gsumxp  20103  pjpm  21921  ptbasfi  23807  mbfmcst  34770  0rrv  34962  inv2  35588  fineqvomon  35644  vonf1wev  35705  vonf1owevOLD  35707  ecqmap  39197  pol0N  40782