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

Theorem inv1 4355
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 4189 . 2 (𝐴 ∩ V) ⊆ 𝐴
2 ssid 3967 . . 3 𝐴𝐴
3 ssv 3969 . . 3 𝐴 ⊆ V
42, 3ssini 4192 . 2 𝐴 ⊆ (𝐴 ∩ V)
51, 4eqssi 3961 1 (𝐴 ∩ V) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Vcvv 3444  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928
This theorem is referenced by:  undif1  4436  dfif4  4502  rint0  4952  iinrab2  5031  riin0  5043  xpriindi  5793  xpssres  5975  resdmdfsn  5988  elrid  6000  imainrect  6134  xpima  6135  cnvrescnv  6148  dmresv  6153  curry1  8037  curry2  8040  fpar  8049  oev2  8470  hashresfn  14246  dmhashres  14247  gsumxp  19758  pjpm  21130  ptbasfi  22948  mbfmcst  32916  0rrv  33108  pol0N  38418
  Copyright terms: Public domain W3C validator