Theorem brabsb

Description: The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008)

	Ref	Expression
Hypothesis	brabsb.1	$$⊢R=\left\{⟨x,y⟩|\phi \right\}$$
Assertion	brabsb	$$⊢ARB\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		brabsb.1	$$⊢R=\left\{⟨x,y⟩|\phi \right\}$$
2		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
3	1	eleq2i	$$⊢⟨A,B⟩\in R\leftrightarrow ⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}$$
4		opelopabsb	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$
5	2 3 4	3bitri	$$⊢ARB\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$