Theorem foeq3 5606

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   ran crn 4828   Fn wfn 5401   -onto->wfo 5404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-fo 5412

This theorem is referenced by:  f1oeq3  5622  foeq123d  5625  resdif  5649  ffoss  6527  fidomdm  7581  fifo  7670  brwdom  7770  brwdom2  7776  canthwdom  7782  ixpiunwdom  7794  fin1a2lem7  8563  znnen  13478  divslem  14464  znzrhfo  17822  rncmp  18841  conima  18871  concn  18872  qtopcmplem  19122  qtoprest  19132  opidon2  23634  pjhfo  24932  dmct  25838  ivthALT  28374