Metamath Proof Explorer

Theorem funbreq

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

Ref Expression
Hypotheses funbreq.1 ${⊢}{A}\in \mathrm{V}$
funbreq.2 ${⊢}{B}\in \mathrm{V}$
funbreq.3 ${⊢}{C}\in \mathrm{V}$
Assertion funbreq ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \left({A}{F}{C}↔{B}={C}\right)$

Proof

Step Hyp Ref Expression
1 funbreq.1 ${⊢}{A}\in \mathrm{V}$
2 funbreq.2 ${⊢}{B}\in \mathrm{V}$
3 funbreq.3 ${⊢}{C}\in \mathrm{V}$
4 1 2 3 fununiq ${⊢}\mathrm{Fun}{F}\to \left(\left({A}{F}{B}\wedge {A}{F}{C}\right)\to {B}={C}\right)$
5 4 expdimp ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \left({A}{F}{C}\to {B}={C}\right)$
6 breq2 ${⊢}{B}={C}\to \left({A}{F}{B}↔{A}{F}{C}\right)$
7 6 biimpcd ${⊢}{A}{F}{B}\to \left({B}={C}\to {A}{F}{C}\right)$
8 7 adantl ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \left({B}={C}\to {A}{F}{C}\right)$
9 5 8 impbid ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \left({A}{F}{C}↔{B}={C}\right)$