Theorem foeq3 5593

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 2244	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 464	. 2 |- ( A = B -> ( ( F Fn C /\ ran F = A ) <-> ( F Fn C /\ ran F = B ) ) )
3		df-fo 5363	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5363	. 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 1398   ran crn 4755   Fn wfn 5352   -onto->wfo 5355

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-fo 5363

This theorem is referenced by:  fimadmfo  5604  f1oeq3  5609  foeq123d  5612  resdif  5641  ffoss  5652  fifo  7280  enumct  7419  ctssexmid  7454  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  qnnen  13266  ctiunctal  13276  unct  13277  quslem  13588  znzrhfo  14922  gausslemma2dlem1f1o  16059  eupthsg  16566  subctctexmid  16900