Theorem foeq2 5797

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

Assertion

Ref	Expression
foeq2

Proof of Theorem foeq2

Step	Hyp	Ref	Expression
1		fneq2 5675	. . 3
2	1	anbi1d 704	. 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:  f1oeq2  5813  foeq123d  5817  tposfo  7001  brwdom  8014  brwdom2  8020  canthwdom  8026  cfslb2n  8669  fodomg  8924  0ramcl  14541  ghmcyg  16898  txcmpb  20145  qtoptopon  20205  opidon2OLD  25326

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-fn 5596  df-fo 5599