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

Step	Hyp	Ref	Expression
1		inss1 3717	. 2
2		ssid 3522	. . 3
3		ssv 3523	. . 3
4	2, 3	ssini 3720	. 2
5	1, 4	eqssi 3519	1

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