Theorem foeq3 5814

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 2473	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 715	. 2 |- ( A = B -> ( ( F Fn C /\ ran F = A ) <-> ( F Fn C /\ ran F = B ) ) )
3		df-fo 5607	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5607	. 2 |- ( F : C -onto-> B <-> ( F Fn C /\ ran F = B ) )
5	2, 3, 4	3bitr4g 296	1 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   ran crn 4854   Fn wfn 5596   -onto->wfo 5599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2455  df-fo 5607

This theorem is referenced by:  f1oeq3  5830  foeq123d  5833  resdif  5857  ffoss  6781  fidomdm  7879  fifo  7972  brwdom  8108  brwdom2  8114  canthwdom  8120  ixpiunwdom  8132  fin1a2lem7  8862  znnen  14314  quslem  15498  znzrhfo  19167  rncmp  20460  conima  20489  concn  20490  qtopcmplem  20771  qtoprest  20781  opidon2OLD  26101  pjhfo  27408  dmct  28347  msrfo  30233  ivthALT  31040  poimirlem26  32011  poimirlem27  32012  founiiun0  37503