Theorem foeq3 5729

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 2469	. . 3 |- ( A = B -> ( ran F = A <-> ran F = B ) )
2	1	anbi2d 703	. 2 |- ( A = B -> ( ( F Fn C /\ ran F = A ) <-> ( F Fn C /\ ran F = B ) ) )
3		df-fo 5535	. 2 |- ( F : C -onto-> A <-> ( F Fn C /\ ran F = A ) )
4		df-fo 5535	. 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 1370   ran crn 4952   Fn wfn 5524   -onto->wfo 5527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fo 5535

This theorem is referenced by:  f1oeq3  5745  foeq123d  5748  resdif  5772  ffoss  6651  fidomdm  7707  fifo  7797  brwdom  7897  brwdom2  7903  canthwdom  7909  ixpiunwdom  7921  fin1a2lem7  8690  znnen  13617  divslem  14604  znzrhfo  18115  rncmp  19141  conima  19171  concn  19172  qtopcmplem  19422  qtoprest  19432  opidon2  23990  pjhfo  25288  dmct  26192  ivthALT  28701