Description: The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brabsb.1 | ⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } | |
Assertion | brabsb | ⊢ ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brabsb.1 | ⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } | |
2 | df-br | ⊢ ( 𝐴 𝑅 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ 𝑅 ) | |
3 | 1 | eleq2i | ⊢ ( 〈 𝐴 , 𝐵 〉 ∈ 𝑅 ↔ 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
4 | opelopabsb | ⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) | |
5 | 2 3 4 | 3bitri | ⊢ ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) |