Description: Converting a class constant definition by restriction (like df-ers or ~? df-parts ) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eqres.1 | |- R = ( S |` C ) |
|
| Assertion | eqres | |- ( B e. V -> ( A R B <-> ( A e. C /\ A S B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqres.1 | |- R = ( S |` C ) |
|
| 2 | 1 | breqi | |- ( A R B <-> A ( S |` C ) B ) |
| 3 | brres | |- ( B e. V -> ( A ( S |` C ) B <-> ( A e. C /\ A S B ) ) ) |
|
| 4 | 2 3 | syl5bb | |- ( B e. V -> ( A R B <-> ( A e. C /\ A S B ) ) ) |