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

Theorem inv1 3812
 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

Proof of Theorem inv1
StepHypRef Expression
1 inss1 3717 . 2
2 ssid 3522 . . 3
3 ssv 3523 . . 3
42, 3ssini 3720 . 2
51, 4eqssi 3519 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395   cvv 3109  i^icin 3474 This theorem is referenced by:  undif1  3903  dfif4  3956  rint0  4327  iinrab2  4393  riin0  4404  xpriindi  5144  xpssres  5313  resdmdfsn  5324  imainrect  5453  xpima  5454  dmresv  5470  curry1  6892  curry2  6895  fpar  6904  oev2  7192  hashresfn  12413  dmhashres  12414  gsumxp  17004  gsumxpOLD  17006  pjpm  18739  ptbasfi  20082  mbfmcst  28230  0rrv  28390  pol0N  35633  xphe  37804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator