Theorem brabd0

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	brabd0.x	$$⊢\phi \to \forall x\phi$$
	brabd0.y	$$⊢\phi \to \forall y\phi$$
	brabd0.xch	$$⊢\phi \to Ⅎx\chi$$
	brabd0.ych	$$⊢\phi \to Ⅎy\chi$$
	brabd0.exa	$$⊢\phi \to A\in U$$
	brabd0.exb	$$⊢\phi \to B\in V$$
	brabd0.def	$$⊢\phi \to R=\left\{⟨x,y⟩|\psi \right\}$$
	brabd0.is	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	brabd0	$$⊢\phi \to \left(ARB\leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		brabd0.x	$$⊢\phi \to \forall x\phi$$
2		brabd0.y	$$⊢\phi \to \forall y\phi$$
3		brabd0.xch	$$⊢\phi \to Ⅎx\chi$$
4		brabd0.ych	$$⊢\phi \to Ⅎy\chi$$
5		brabd0.exa	$$⊢\phi \to A\in U$$
6		brabd0.exb	$$⊢\phi \to B\in V$$
7		brabd0.def	$$⊢\phi \to R=\left\{⟨x,y⟩|\psi \right\}$$
8		brabd0.is	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
9		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
10	7	eleq2d	$$⊢\phi \to \left(⟨A,B⟩\in R\leftrightarrow ⟨A,B⟩\in \left\{⟨x,y⟩|\psi \right\}\right)$$
11	9 10	syl5bb	$$⊢\phi \to \left(ARB\leftrightarrow ⟨A,B⟩\in \left\{⟨x,y⟩|\psi \right\}\right)$$
12	1 2 3 4 5 6 8	opelopabd	$$⊢\phi \to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \chi \right)$$
13	11 12	bitrd	$$⊢\phi \to \left(ARB\leftrightarrow \chi \right)$$