Theorem elimaint

Description: Element of image of intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	elimaint	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2	1	elima	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑏 ∩ 𝐴 𝑦 )
3		df-br	⊢ ( 𝑏 ∩ 𝐴 𝑦 ↔ ⟨ 𝑏 , 𝑦 ⟩ ∈ ∩ 𝐴 )
4		opex	⊢ ⟨ 𝑏 , 𝑦 ⟩ ∈ V
5	4	elint2	⊢ ( ⟨ 𝑏 , 𝑦 ⟩ ∈ ∩ 𝐴 ↔ ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
6	3 5	bitri	⊢ ( 𝑏 ∩ 𝐴 𝑦 ↔ ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
7	6	rexbii	⊢ ( ∃ 𝑏 ∈ 𝐵 𝑏 ∩ 𝐴 𝑦 ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
8	2 7	bitri	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )