Theorem foeq3 5554

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 2239	. . 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 5330	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5330	. 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 1395   ran crn 4724   Fn wfn 5319   -onto->wfo 5322

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-fo 5330

This theorem is referenced by:  fimadmfo  5565  f1oeq3  5570  foeq123d  5573  resdif  5602  ffoss  5612  fifo  7170  enumct  7305  ctssexmid  7340  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  qnnen  13042  ctiunctal  13052  unct  13053  quslem  13397  znzrhfo  14652  gausslemma2dlem1f1o  15779  eupthsg  16240  subctctexmid  16537