Description: The law of concretion for a binary relation. Special case of brabga . Usage of this theorem is discouraged because it depends on ax-13 , see brabidgaw for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | brabidga.1 | |- R = { <. x , y >. | ph } |
|
| Assertion | brabidga | |- ( x R y <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brabidga.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 | opabid | |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |
|
| 5 | 2 3 4 | 3bitri | |- ( x R y <-> ph ) |