Theorem brintclab

Description: Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020)

	Ref	Expression
Assertion	brintclab	⊢ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } 𝐵 ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } )
2		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
3	2	elintab	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑥 ) )
4	1 3	bitri	⊢ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } 𝐵 ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑥 ) )