Theorem foeq3 5498

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 2215	. . 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 5278	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5278	. 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 1373   ran crn 4677   Fn wfn 5267   -onto->wfo 5270

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-fo 5278

This theorem is referenced by:  fimadmfo  5509  f1oeq3  5514  foeq123d  5517  resdif  5546  ffoss  5556  fifo  7084  enumct  7219  ctssexmid  7254  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  qnnen  12835  ctiunctal  12845  unct  12846  quslem  13189  znzrhfo  14443  gausslemma2dlem1f1o  15570  subctctexmid  15974