Theorem intimasn

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	intimasn	⊢ ( 𝐵 ∈ 𝑉 → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ { 𝐵 } ) } )

Proof

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( 𝐵 ∈ 𝑉 → ∀ 𝑦 𝐵 ∈ 𝑉 )
2		r19.12sn	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑏 ∈ { 𝐵 } ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝐵 } ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
3	2	biimprd	⊢ ( 𝐵 ∈ 𝑉 → ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝐵 } ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ { 𝐵 } ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
4	3	alimi	⊢ ( ∀ 𝑦 𝐵 ∈ 𝑉 → ∀ 𝑦 ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝐵 } ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ { 𝐵 } ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
5		intimag	⊢ ( ∀ 𝑦 ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝐵 } ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ { 𝐵 } ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ { 𝐵 } ) } )
6	1 4 5	3syl	⊢ ( 𝐵 ∈ 𝑉 → ( ∩ 𝐴 “ { 𝐵 } ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ { 𝐵 } ) } )