Theorem inv1 4404

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 4245	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 4018	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 4020	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4248	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 4012	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1537  Vcvv 3478   ∩ cin 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ss 3980

This theorem is referenced by:  undif1  4482  dfif4  4546  rint0  4993  iinrab2  5075  riin0  5087  xpriindi  5850  xpssres  6038  resdmdfsn  6051  elrid  6066  imainrect  6203  xpima  6204  cnvrescnv  6217  dmresv  6222  curry1  8128  curry2  8131  fpar  8140  oev2  8560  hashresfn  14376  dmhashres  14377  gsumxp  20009  pjpm  21746  ptbasfi  23605  mbfmcst  34241  0rrv  34433  pol0N  39892