Description: If a binary relation holds and the relation is the value of a function, then the argument to that function is a set. (Contributed by RP, 22-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | brfvimex.br | |- ( ph -> A R B ) |
|
| brfvimex.fv | |- ( ph -> R = ( F ` C ) ) |
||
| Assertion | brfvimex | |- ( ph -> C e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brfvimex.br | |- ( ph -> A R B ) |
|
| 2 | brfvimex.fv | |- ( ph -> R = ( F ` C ) ) |
|
| 3 | 2 1 | breqdi | |- ( ph -> A ( F ` C ) B ) |
| 4 | brne0 | |- ( A ( F ` C ) B -> ( F ` C ) =/= (/) ) |
|
| 5 | fvprc | |- ( -. C e. _V -> ( F ` C ) = (/) ) |
|
| 6 | 5 | necon1ai | |- ( ( F ` C ) =/= (/) -> C e. _V ) |
| 7 | 3 4 6 | 3syl | |- ( ph -> C e. _V ) |