Theorem intunsn

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

	Ref	Expression
Hypothesis	intunsn.1	⊢ 𝐵 ∈ V
Assertion	intunsn	⊢ ∩ ( 𝐴 ∪ { 𝐵 } ) = ( ∩ 𝐴 ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		intunsn.1	⊢ 𝐵 ∈ V
2		intun	⊢ ∩ ( 𝐴 ∪ { 𝐵 } ) = ( ∩ 𝐴 ∩ ∩ { 𝐵 } )
3	1	intsn	⊢ ∩ { 𝐵 } = 𝐵
4	3	ineq2i	⊢ ( ∩ 𝐴 ∩ ∩ { 𝐵 } ) = ( ∩ 𝐴 ∩ 𝐵 )
5	2 4	eqtri	⊢ ∩ ( 𝐴 ∪ { 𝐵 } ) = ( ∩ 𝐴 ∩ 𝐵 )