Theorem 0in 3969

Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
0in	|- ( (/) i^i A ) = (/)

Proof of Theorem 0in

Step	Hyp	Ref	Expression
1		incom 3805	. 2 |- ( (/) i^i A ) = ( A i^i (/) )
2		in0 3968	. 2 |- ( A i^i (/) ) = (/)
3	1, 2	eqtri 2644	1 |- ( (/) i^i A ) = (/)

Syntax hints:   = wceq 1483   i^i cin 3573   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916

This theorem is referenced by:  pred0  5710  fnsuppeq0  7323  setsfun  15893  setsfun0  15894  indistopon  20805  fctop  20808  cctop  20810  restsn  20974  filconn  21687  chtdif  24884  ppidif  24889  ppi1  24890  cht1  24891  ofpreima2  29466  ordtconnlem1  29970  measvuni  30277  measinb  30284  cndprobnul  30499  ballotlemfp1  30553  ballotlemgun  30586  chtvalz  30707  mrsubvrs  31419  mblfinlem2  33447  ntrkbimka  38336  limsup0  39926  subsalsal  40577  nnfoctbdjlem  40672