Metamath Proof Explorer


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 ( 𝐴 𝑅 𝐵[ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )