Theorem foeq3 5798

Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
foeq3

Proof of Theorem foeq3

Step	Hyp	Ref	Expression
1		eqeq2 2472	. . 3
2	1	anbi2d 703	. 2
3		df-fo 5599	. 2
4		df-fo 5599	. 2
5	2, 3, 4	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  rancrn 5005  Fnwfn 5588  -onto->wfo 5591

This theorem is referenced by:  f1oeq3  5814  foeq123d  5817  resdif  5841  ffoss  6761  fidomdm  7822  fifo  7912  brwdom  8014  brwdom2  8020  canthwdom  8026  ixpiunwdom  8038  fin1a2lem7  8807  znnen  13946  quslem  14940  znzrhfo  18586  rncmp  19896  conima  19926  concn  19927  qtopcmplem  20208  qtoprest  20218  opidon2OLD  25326  pjhfo  26624  dmct  27537  msrfo  28906  ivthALT  30153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fo 5599