Theorem foeq3 5608

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   ran crn 4770   Fn wfn 5367   -onto->wfo 5370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fo 5378

This theorem is referenced by:  fimadmfo  5619  f1oeq3  5624  foeq123d  5627  resdif  5656  ffoss  5667  fifo  7304  enumct  7445  ctssexmid  7480  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  qnnen  13300  ctiunctal  13310  unct  13311  quslem  13622  znzrhfo  14955  gausslemma2dlem1f1o  16093  eupthsg  16600  subctctexmid  16944