Theorem brrabga

Description: The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022)

	Ref	Expression
Hypotheses	brrabga.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
	brrabga.2	$$⊢R=\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
Assertion	brrabga	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(⟨A,B⟩RC\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		brrabga.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		brrabga.2	$$⊢R=\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
3		df-br	$$⊢⟨A,B⟩RC\leftrightarrow ⟨⟨A,B⟩,C⟩\in R$$
4	2	eleq2i	$$⊢⟨⟨A,B⟩,C⟩\in R\leftrightarrow ⟨⟨A,B⟩,C⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
5	3 4	bitri	$$⊢⟨A,B⟩RC\leftrightarrow ⟨⟨A,B⟩,C⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
6	1	eloprabga	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(⟨⟨A,B⟩,C⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \psi \right)$$
7	5 6	bitrid	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(⟨A,B⟩RC\leftrightarrow \psi \right)$$