Theorem foeq3 5610

Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)

Assertion

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

Proof of Theorem foeq3

Step	Hyp	Ref	Expression
1		eqeq2 2413	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 685	. 2 |- ( A = B -> ( ( F Fn C /\ ran F = A ) <-> ( F Fn C /\ ran F = B ) ) )
3		df-fo 5419	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5419	. 2 |- ( F : C -onto-> B <-> ( F Fn C /\ ran F = B ) )
5	2, 3, 4	3bitr4g 280	1 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   ran crn 4838   Fn wfn 5408   -onto->wfo 5411

This theorem is referenced by:  f1oeq3  5626  foeq123d  5629  resdif  5655  ffoss  5666  fidomdm  7347  fifo  7395  brwdom  7491  brwdom2  7497  canthwdom  7503  ixpiunwdom  7515  fin1a2lem7  8242  znnen  12767  divslem  13723  znzrhfo  16783  rncmp  17413  conima  17441  concn  17442  qtopcmplem  17692  qtoprest  17702  opidon2  21865  pjhfo  23161  dmct  24059  ivthALT  26228

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-fo 5419