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  7455  ctssexmid  7490  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  qnnen  13371  ctiunctal  13381  unct  13382  quslem  13694  znzrhfo  15032  gausslemma2dlem1f1o  16277  eupthsg  16784  subctctexmid  17128