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 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 5383	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5383	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   ran crn 4775   Fn wfn 5372   -onto->wfo 5375

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fo 5383

This theorem is used by:  fimadmfo  5624  f1oeq3  5629  foeq123d  5632  resdif  5661  ffoss  5672  fifo  7314  enumct  7456  ctssexmid  7491  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  qnnen  13374  ctiunctal  13384  unct  13385  quslem  13698  znzrhfo  15067  gausslemma2dlem1f1o  16345  eupthsg  16852  subctctexmid  17196