MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inv1 Structured version   Visualization version   GIF version

Theorem inv1 4324
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
StepHypRef Expression
1 inss1 4183 . 2 (𝐴 ∩ V) ⊆ 𝐴
2 ssid 3968 . . 3 𝐴𝐴
3 ssv 3970 . . 3 𝐴 ⊆ V
42, 3ssini 4186 . 2 𝐴 ⊆ (𝐴 ∩ V)
51, 4eqssi 3962 1 (𝐴 ∩ V) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  Vcvv 3473  cin 3912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-in 3920  df-ss 3930
This theorem is referenced by:  undif1  4400  dfif4  4458  rint0  4892  iinrab2  4968  riin0  4980  xpriindi  5683  xpssres  5865  resdmdfsn  5877  elrid  5889  imainrect  6014  xpima  6015  cnvrescnv  6028  dmresv  6033  curry1  7777  curry2  7780  fpar  7789  oev2  8126  hashresfn  13685  dmhashres  13686  gsumxp  19075  pjpm  20828  ptbasfi  22165  mbfmcst  31525  0rrv  31717  pol0N  37081
  Copyright terms: Public domain W3C validator