Theorem intimasn2

Description: Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimasn2	⊢ ( 𝐵 ∈ 𝑉 → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		intimasn	⊢ ( 𝐵 ∈ 𝑉 → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑥 “ { 𝐵 } ) } )
2		intima0	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ { 𝐵 } ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑥 “ { 𝐵 } ) }
3	1 2	eqtr4di	⊢ ( 𝐵 ∈ 𝑉 → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ { 𝐵 } ) )