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

Metamath Proof Explorer

Theorem fvelrnbf

Description: A version of fvelrnb using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fvelrnbf.1 ⊢ Ⅎ _ x A
fvelrnbf.2 ⊢ Ⅎ _ x B
fvelrnbf.3 ⊢ Ⅎ _ x F
Assertion fvelrnbf ⊢ F Fn A → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ⁡ x = B

Proof

Step Hyp Ref Expression
1 fvelrnbf.1 ⊢ Ⅎ _ x A
2 fvelrnbf.2 ⊢ Ⅎ _ x B
3 fvelrnbf.3 ⊢ Ⅎ _ x F
4 fvelrnb ⊢ F Fn A → B ∈ ran ⁡ F ↔ ∃ y ∈ A F ⁡ y = B
5 nfcv ⊢ Ⅎ _ y A
6 nfcv ⊢ Ⅎ _ x y
7 3 6 nffv ⊢ Ⅎ _ x F ⁡ y
8 7 2 nfeq ⊢ Ⅎ x F ⁡ y = B
9 nfv ⊢ Ⅎ y F ⁡ x = B
10 fveqeq2 ⊢ y = x → F ⁡ y = B ↔ F ⁡ x = B
11 5 1 8 9 10 cbvrexfw ⊢ ∃ y ∈ A F ⁡ y = B ↔ ∃ x ∈ A F ⁡ x = B
12 4 11 bitrdi ⊢ F Fn A → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ⁡ x = B