Theorem feq3 3622

Description: Equality theorem for functions.

Assertion

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

Proof of Theorem feq3

Step	Hyp	Ref	Expression
1		sseq2 2083	. . 3 |- (A = B -> (ran F (_ A <-> ran F (_ B))
2	1	anbi2d 616	. 2 |- (A = B -> ((F Fn C /\ ran F (_ A) <-> (F Fn C /\ ran F (_ B)))
3		df-f 3194	. 2 |- (F:C-->A <-> (F Fn C /\ ran F (_ A))
4		df-f 3194	. 2 |- (F:C-->B <-> (F Fn C /\ ran F (_ B))
5	2, 3, 4	3bitr4g 555	1 |- (A = B -> (F:C-->A <-> F:C-->B))

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:  fconstg 3659  f1eq3 3662  fsn2 3836  mapvalg 4330  mapsn 4345  mapdom2 4494  mapunen 4502  cncfval 7264  metcnpf 7883  metcnf 7884  lmsslem 7952  metcn4 7971  cmsss 7997  bcthlem22 8020  bcth 8032  isgrp 8041  isring 8141  ringi 8142  vci 8167  isvclem 8196  vcoprnelem 8197  nvcnf 8327  nvcnpf 8328  lnoval 8413  nmofval 8425  ajfval 8469  ubthlem3 8531  closedsub 9093  ch2 9114  nmop0h 9916  elghomlem1 10382  ghomgrpilem2 10386  cnrscoa 10510  ismgra 10642  isalg 10653  algi 10660  aidm 10683  aidmold 10684  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-f 3194

Copyright terms: Public domain