Theorem foeq3 6113

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 2633	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 740	. 2 |- ( A = B -> ( ( F Fn C /\ ran F = A ) <-> ( F Fn C /\ ran F = B ) ) )
3		df-fo 5894	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5894	. 2 |- ( F : C -onto-> B <-> ( F Fn C /\ ran F = B ) )
5	2, 3, 4	3bitr4g 303	1 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   ran crn 5115   Fn wfn 5883   -onto->wfo 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fo 5894

This theorem is referenced by:  f1oeq3  6129  foeq123d  6132  resdif  6157  ffoss  7127  rneqdmfinf1o  8242  fidomdm  8243  fifo  8338  brwdom  8472  brwdom2  8478  canthwdom  8484  ixpiunwdom  8496  fin1a2lem7  9228  dmct  9346  znnen  14941  quslem  16203  znzrhfo  19896  rncmp  21199  connima  21228  conncn  21229  qtopcmplem  21510  qtoprest  21520  eupths  27060  pjhfo  28565  msrfo  31443  ivthALT  32330  poimirlem26  33435  poimirlem27  33436  opidon2OLD  33653  founiiun0  39377