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	$$⊢A\bigcap \left\{x|\phi \right\}B\leftrightarrow \forall x\left(\phi \to ⟨A,B⟩\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢A\bigcap \left\{x|\phi \right\}B\leftrightarrow ⟨A,B⟩\in \bigcap \left\{x|\phi \right\}$$
2		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
3	2	elintab	$$⊢⟨A,B⟩\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to ⟨A,B⟩\in x\right)$$
4	1 3	bitri	$$⊢A\bigcap \left\{x|\phi \right\}B\leftrightarrow \forall x\left(\phi \to ⟨A,B⟩\in x\right)$$