Theorem feq2 3621

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 3583	. . 3 |- (A = B -> (F Fn A <-> F Fn B))
2	1	anbi1d 617	. 2 |- (A = B -> ((F Fn A /\ ran F (_ C) <-> (F Fn B /\ ran F (_ C)))
3		df-f 3194	. 2 |- (F:A-->C <-> (F Fn A /\ ran F (_ C))
4		df-f 3194	. 2 |- (F:B-->C <-> (F Fn B /\ ran F (_ C))
5	2, 3, 4	3bitr4g 555	1 |- (A = B -> (F:A-->C <-> F:B-->C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   (_ wss 2047  ran crn 3171   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  ffdm 3639  f00 3657  fconst 3658  f1eq2 3661  fressnfv 3838  fconstfv 3849  mapvalg 4330  mapdom2 4494  ser0mulc 7059  ser1mulc 7060  isum0split 7217  geolim1i 7238  cncfval 7264  eftlexOLD 7377  efsep 7396  effsumle 7397  efm1lim 7411  ismet 7798  dfms2 7799  ismsg 7800  msflem 7803  metreslem 7822  0met 7825  metcnpf 7883  metcnf 7884  metcnconst 7885  metdnsconst 7901  metcn4 7971  isgrp 8041  grpsn 8124  isring 8141  ringi 8142  vci 8167  isvclem 8196  vcoprnelem 8197  isnvlem 8229  nvi 8233  nvcnf 8327  nvcnpf 8328  lnoval 8413  nmofval 8425  ajfval 8469  elghomlem1 10382  cnrsfin 10509  ismgra 10642  isalg 10653  algi 10660  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469  df-fn 3193  df-f 3194

Copyright terms: Public domain