Theorem brabsb

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

	Ref	Expression
Hypothesis	brabsb.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion	brabsb	⊢ ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		brabsb.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
3	1	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
4		opelopabsb	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
5	2 3 4	3bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )