Theorem inv1 4326

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 4165	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3937	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3939	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4168	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3931	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1547  Vcvv 3431   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  undif1  4404  dfif4  4470  rint0  4918  iinrab2  4999  riin0  5011  xpriindi  5778  xpssres  5970  resdmdfsn  5983  elrid  5998  imainrect  6132  xpima  6133  cnvrescnv  6146  dmresv  6151  curry1  8043  curry2  8046  fpar  8055  oev2  8448  hashresfn  14293  dmhashres  14294  gsumxp  19942  pjpm  21683  ptbasfi  23564  mbfmcst  34443  0rrv  34635  fineqvomon  35299  vonf1owev  35336  ecqmap  38816  pol0N  40401