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

Metamath Proof Explorer

Theorem funbrfv

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion funbrfv ⊢ Fun ⁡ F → A F B → F ⁡ A = B

Proof

Step Hyp Ref Expression
1 funrel ⊢ Fun ⁡ F → Rel ⁡ F
2 brrelex2 ⊢ Rel ⁡ F ∧ A F B → B ∈ V
3 1 2 sylan ⊢ Fun ⁡ F ∧ A F B → B ∈ V
4 breq2 ⊢ y = B → A F y ↔ A F B
5 4 anbi2d ⊢ y = B → Fun ⁡ F ∧ A F y ↔ Fun ⁡ F ∧ A F B
6 eqeq2 ⊢ y = B → F ⁡ A = y ↔ F ⁡ A = B
7 5 6 imbi12d ⊢ y = B → Fun ⁡ F ∧ A F y → F ⁡ A = y ↔ Fun ⁡ F ∧ A F B → F ⁡ A = B
8 funeu ⊢ Fun ⁡ F ∧ A F y → ∃! y A F y
9 tz6.12-1 ⊢ A F y ∧ ∃! y A F y → F ⁡ A = y
10 8 9 sylan2 ⊢ A F y ∧ Fun ⁡ F ∧ A F y → F ⁡ A = y
11 10 anabss7 ⊢ Fun ⁡ F ∧ A F y → F ⁡ A = y
12 7 11 vtoclg ⊢ B ∈ V → Fun ⁡ F ∧ A F B → F ⁡ A = B
13 3 12 mpcom ⊢ Fun ⁡ F ∧ A F B → F ⁡ A = B
14 13 ex ⊢ Fun ⁡ F → A F B → F ⁡ A = B