Theorem foeq3 5613

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 2447	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 703	. 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 288	1 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   ran crn 4836   Fn wfn 5408   -onto->wfo 5411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-fo 5419

This theorem is referenced by:  f1oeq3  5629  foeq123d  5632  resdif  5656  ffoss  6533  fidomdm  7585  fifo  7674  brwdom  7774  brwdom2  7780  canthwdom  7786  ixpiunwdom  7798  fin1a2lem7  8567  znnen  13487  divslem  14473  znzrhfo  17955  rncmp  18974  conima  19004  concn  19005  qtopcmplem  19255  qtoprest  19265  opidon2  23762  pjhfo  25060  dmct  25965  ivthALT  28483