Theorem intunsn

Description: Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002)

	Ref	Expression
Hypothesis	intunsn.1	|- B e. _V
Assertion	intunsn	|- |^| ( A u. { B } ) = ( |^| A i^i B )

Proof

Step	Hyp	Ref	Expression
1		intunsn.1	|- B e. _V
2		intun	|- |^| ( A u. { B } ) = ( |^| A i^i |^| { B } )
3	1	intsn	|- |^| { B } = B
4	3	ineq2i	|- ( |^| A i^i |^| { B } ) = ( |^| A i^i B )
5	2 4	eqtri	|- |^| ( A u. { B } ) = ( |^| A i^i B )