Theorem inv1 4352

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 4188	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3958	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3960	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4191	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3952	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1560  Vcvv 3454   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ss 3921

This theorem is referenced by:  undif1  4430  dfif4  4496  rint0  4946  iinrab2  5027  riin0  5039  xpriindi  5808  xpssres  6004  resdmdfsn  6018  resdmdfsnOLD  6019  elrid  6035  imainrect  6167  xpima  6168  cnvrescnv  6182  dmresv  6187  curry1  8083  curry2  8086  fpar  8095  oev2  8492  hashresfn  14353  dmhashres  14354  gsumxp  20016  pjpm  21757  ptbasfi  23638  mbfmcst  34553  0rrv  34745  fineqvomon  35411  vonf1wev  35448  vonf1owevOLD  35450  ecqmap  38945  pol0N  40530