Metamath Proof Explorer

Theorem funbreq

Description: An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypotheses funbreq.1 ⊢ A ∈ V
funbreq.2 ⊢ B ∈ V
funbreq.3 ⊢ C ∈ V
Assertion funbreq ⊢ Fun ⁡ F ∧ A F B → A F C ↔ B = C

Proof

Step Hyp Ref Expression
1 funbreq.1 ⊢ A ∈ V
2 funbreq.2 ⊢ B ∈ V
3 funbreq.3 ⊢ C ∈ V
4 1 2 3 fununiq ⊢ Fun ⁡ F → A F B ∧ A F C → B = C
5 4 expdimp ⊢ Fun ⁡ F ∧ A F B → A F C → B = C
6 breq2 ⊢ B = C → A F B ↔ A F C
7 6 biimpcd ⊢ A F B → B = C → A F C
8 7 adantl ⊢ Fun ⁡ F ∧ A F B → B = C → A F C
9 5 8 impbid ⊢ Fun ⁡ F ∧ A F B → A F C ↔ B = C