Metamath Proof Explorer

Theorem afvelrnb

Description: A member of a function's range is a value of the function, analogous to fvelrnb with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afvelrnb ⊢FFnA∧B∈V→B∈ran⁡F↔∃x∈AF'''x=B

Proof

Step Hyp Ref Expression
1 fnrnafv ⊢FFnA→ran⁡F=y|∃x∈Ay=F'''x
2 1 adantr ⊢FFnA∧B∈V→ran⁡F=y|∃x∈Ay=F'''x
3 2 eleq2d ⊢FFnA∧B∈V→B∈ran⁡F↔B∈y|∃x∈Ay=F'''x
4 eqeq1 ⊢y=B→y=F'''x↔B=F'''x
5 eqcom ⊢B=F'''x↔F'''x=B
6 4 5 bitrdi ⊢y=B→y=F'''x↔F'''x=B
7 6 rexbidv ⊢y=B→∃x∈Ay=F'''x↔∃x∈AF'''x=B
8 7 elabg ⊢B∈V→B∈y|∃x∈Ay=F'''x↔∃x∈AF'''x=B
9 8 adantl ⊢FFnA∧B∈V→B∈y|∃x∈Ay=F'''x↔∃x∈AF'''x=B
10 3 9 bitrd ⊢FFnA∧B∈V→B∈ran⁡F↔∃x∈AF'''x=B