Theorem foeq3 5799

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 2482	. . 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 5600	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5600	. 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 1379   ran crn 5006   Fn wfn 5589   -onto->wfo 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fo 5600

This theorem is referenced by:  f1oeq3  5815  foeq123d  5818  resdif  5842  ffoss  6756  fidomdm  7814  fifo  7904  brwdom  8005  brwdom2  8011  canthwdom  8017  ixpiunwdom  8029  fin1a2lem7  8798  znnen  13824  quslem  14815  znzrhfo  18455  rncmp  19764  conima  19794  concn  19795  qtopcmplem  20076  qtoprest  20086  opidon2OLD  25149  pjhfo  26447  dmct  27360  msrfo  28731  ivthALT  30080