Description: If two elements are connected by a value of the identity relation, then they are connected via the argument. (Contributed by RP, 21-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | brfvid.r | |- ( ph -> R e. _V ) |
|
| Assertion | brfvid | |- ( ph -> ( A ( _I ` R ) B <-> A R B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brfvid.r | |- ( ph -> R e. _V ) |
|
| 2 | fvi | |- ( R e. _V -> ( _I ` R ) = R ) |
|
| 3 | 1 2 | syl | |- ( ph -> ( _I ` R ) = R ) |
| 4 | 3 | breqd | |- ( ph -> ( A ( _I ` R ) B <-> A R B ) ) |