Description: The law of concretion for a binary relation. Special case of brabga . Version of brabidga with a disjoint variable condition, which does not require ax-13 . (Contributed by Peter Mazsa, 24-Nov-2018) (Revised by Gino Giotto, 2-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brabidgaw.1 | ⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } | |
Assertion | brabidgaw | ⊢ ( 𝑥 𝑅 𝑦 ↔ 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brabidgaw.1 | ⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } | |
2 | 1 | breqi | ⊢ ( 𝑥 𝑅 𝑦 ↔ 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑦 ) |
3 | df-br | ⊢ ( 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) | |
4 | opabidw | ⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 𝜑 ) | |
5 | 2 3 4 | 3bitri | ⊢ ( 𝑥 𝑅 𝑦 ↔ 𝜑 ) |