Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | feq1 | |- ( F = G -> ( F : A --> B <-> G : A --> B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 | |- ( F = G -> ( F Fn A <-> G Fn A ) ) |
|
2 | rneq | |- ( F = G -> ran F = ran G ) |
|
3 | 2 | sseq1d | |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) ) |
4 | 1 3 | anbi12d | |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) ) |
5 | df-f | |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) |
|
6 | df-f | |- ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) ) |
|
7 | 4 5 6 | 3bitr4g | |- ( F = G -> ( F : A --> B <-> G : A --> B ) ) |