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 3451   ∩ 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  vvin  4359  undif1  4430  dfif4  4498  rint0  4948  iinrab2  5028  riin0  5042  xpriindi  5813  xpssres  6007  resdmdfsn  6021  resdmdfsnOLD  6022  elrid  6038  imainrect  6173  xpima  6174  cnvrescnv  6188  dmresv  6193  imadifssranOLD  6201  curry1  8113  curry2  8116  fpar  8125  oev2  8524  hashresfn  14477  dmhashres  14478  gsumxp  20183  pjpm  22007  ptbasfi  23893  mbfmcst  34884  0rrv  35076  inv2  35702  fineqvomon  35769  vonf1wev  35870  vonf1owevOLD  35872  ecqmap  39361  pol0N  40946