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

Theorem inv1 3942
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 3811 . 2 (𝐴 ∩ V) ⊆ 𝐴
2 ssid 3603 . . 3 𝐴𝐴
3 ssv 3604 . . 3 𝐴 ⊆ V
42, 3ssini 3814 . 2 𝐴 ⊆ (𝐴 ∩ V)
51, 4eqssi 3599 1 (𝐴 ∩ V) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  Vcvv 3186  cin 3554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562  df-ss 3569
This theorem is referenced by:  undif1  4015  dfif4  4073  rint0  4482  iinrab2  4549  riin0  4560  xpriindi  5218  xpssres  5393  resdmdfsn  5404  imainrect  5534  xpima  5535  dmresv  5552  curry1  7214  curry2  7217  fpar  7226  oev2  7548  hashresfn  13068  dmhashres  13069  gsumxp  18296  pjpm  19971  ptbasfi  21294  mbfmcst  30099  0rrv  30291  pol0N  34672
  Copyright terms: Public domain W3C validator