Theorem foeq3 5474

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 2203	. . 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 5260	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5260	. 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 1364   ran crn 4660   Fn wfn 5249   -onto->wfo 5252

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fo 5260

This theorem is referenced by:  fimadmfo  5485  f1oeq3  5490  foeq123d  5493  resdif  5522  ffoss  5532  fifo  7039  enumct  7174  ctssexmid  7209  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  qnnen  12588  ctiunctal  12598  unct  12599  quslem  12907  znzrhfo  14136  gausslemma2dlem1f1o  15176  subctctexmid  15491