Theorem foeq3 5475

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 5261	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5261	. 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 4661   Fn wfn 5250   -onto->wfo 5253

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 5261

This theorem is referenced by:  fimadmfo  5486  f1oeq3  5491  foeq123d  5494  resdif  5523  ffoss  5533  fifo  7041  enumct  7176  ctssexmid  7211  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  qnnen  12591  ctiunctal  12601  unct  12602  quslem  12910  znzrhfo  14147  gausslemma2dlem1f1o  15217  subctctexmid  15561