This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfv2ex

Description: If a function value of a function value has a member, then the first argument is a set. (Contributed by AV, 8-Apr-2021)

Ref Expression
Assertion elfv2ex ⊢ A ∈ F ⁡ B ⁡ C → B ∈ V

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ B ∈ V → A ∈ F ⁡ B ⁡ C → B ∈ V
2 fv2prc ⊢ ¬ B ∈ V → F ⁡ B ⁡ C = ∅
3 2 eleq2d ⊢ ¬ B ∈ V → A ∈ F ⁡ B ⁡ C ↔ A ∈ ∅
4 noel ⊢ ¬ A ∈ ∅
5 4 pm2.21i ⊢ A ∈ ∅ → B ∈ V
6 3 5 biimtrdi ⊢ ¬ B ∈ V → A ∈ F ⁡ B ⁡ C → B ∈ V
7 1 6 pm2.61i ⊢ A ∈ F ⁡ B ⁡ C → B ∈ V