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 | |- R = { <. x , y >. | ph } |
|
| Assertion | brabidgaw | |- ( x R y <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brabidgaw.1 | |- R = { <. x , y >. | ph } |
|
| 2 | 1 | breqi | |- ( x R y <-> x { <. x , y >. | ph } y ) |
| 3 | df-br | |- ( x { <. x , y >. | ph } y <-> <. x , y >. e. { <. x , y >. | ph } ) |
|
| 4 | opabidw | |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |
|
| 5 | 2 3 4 | 3bitri | |- ( x R y <-> ph ) |