Theorem feq2 3627

Description: Equality theorem for functions.

Assertion

Ref	Expression
feq2	|- (A = B -> (F:A-->C <-> F:B-->C))

Proof of Theorem feq2

Step	Hyp	Ref	Expression
1		fneq2 3589	. . 3 |- (A = B -> (F Fn A <-> F Fn B))
2	1	anbi1d 619	. 2 |- (A = B -> ((F Fn A /\ ran F (_ C) <-> (F Fn B /\ ran F (_ C)))
3		df-f 3200	. 2 |- (F:A-->C <-> (F Fn A /\ ran F (_ C))
4		df-f 3200	. 2 |- (F:B-->C <-> (F Fn B /\ ran F (_ C))
5	2, 3, 4	3bitr4g 557	1 |- (A = B -> (F:A-->C <-> F:B-->C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   (_ wss 2050  ran crn 3177   Fn wfn 3183  -->wf 3184

This theorem is referenced by:  ffdm 3645  f00 3663  fconst 3664  f1eq2 3667  fressnfv 3844  fconstfv 3855  mapvalg 4336  mapdom2 4500  ser0mulc 7059  ser1mulc 7060  isum0split 7217  geolim1i 7238  cncfval 7264  eftlexOLD 7377  efsep 7396  effsumle 7397  efm1lim 7411  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  0met 7822  metcnpf 7880  metcnf 7881  metcnconst 7882  metdnsconst 7898  metcn4 7968  isgrp 8038  grpsn 8120  isring 8137  ringi 8138  vci 8163  isvclem 8192  vcoprnelem 8193  isnvlem 8225  nvi 8229  nvcnf 8323  nvcnpf 8324  lnoval 8409  nmofval 8421  ajfval 8465  elghomlem1 10377  cnrsfin 10495  ismgra 10613  isalg 10624  algi 10631  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472  df-fn 3199  df-f 3200

Copyright terms: Public domain