Theorem foeq3 5804

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   ran crn 4850   Fn wfn 5592   -onto->wfo 5595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414  df-fo 5603

This theorem is referenced by:  f1oeq3  5820  foeq123d  5823  resdif  5847  ffoss  6764  fidomdm  7855  fifo  7948  brwdom  8084  brwdom2  8090  canthwdom  8096  ixpiunwdom  8108  fin1a2lem7  8836  znnen  14252  quslem  15436  znzrhfo  19104  rncmp  20397  conima  20426  concn  20427  qtopcmplem  20708  qtoprest  20718  opidon2OLD  26037  pjhfo  27344  dmct  28291  msrfo  30179  ivthALT  30983  poimirlem26  31879  poimirlem27  31880  founiiun0  37314