Theorem f1oeq1 5607

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1oeq1	|- ( F = G -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )

Proof of Theorem f1oeq1

Step	Hyp	Ref	Expression
1		f1eq1 5573	. . 3 |- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )
2		foeq1 5591	. . 3 |- ( F = G -> ( F : A -onto-> B <-> G : A -onto-> B ) )
3	1, 2	anbi12d 473	. 2 |- ( F = G -> ( ( F : A -1-1-> B /\ F : A -onto-> B ) <-> ( G : A -1-1-> B /\ G : A -onto-> B ) ) )
4		df-f1o 5364	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
5		df-f1o 5364	. 2 |- ( G : A -1-1-onto-> B <-> ( G : A -1-1-> B /\ G : A -onto-> B ) )
6	3, 4, 5	3bitr4g 223	1 |- ( F = G -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   -1-1->wf1 5354   -onto->wfo 5355   -1-1-onto->wf1o 5356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115  df-opab 4177  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364

This theorem is referenced by:  f1oeq123d  5613  f1oeq1d  5614  f1ocnvb  5633  f1orescnv  5635  f1ovi  5660  f1osng  5662  f1oresrab  5847  fsn  5854  isoeq1  5980  mapsnd  6936  mapsn  6938  mapsnf1o3  6945  f1oen4g  7004  f1oen3g  7006  ensn1  7049  en2prd  7072  xpcomf1o  7089  xpen  7111  seq3f1olemstep  10900  seq3f1olemp  10901  seqf1oglem2  10906  seqf1og  10907  fihasheqf1oi  11175  fihashf1rn  11176  hashfacen  11233  fzf1o  12086  summodc  12094  fsum3  12098  prodmodc  12289  fprodseq  12294  eulerthlemh  12953  gfsumval  14102  relogf1o  15852  2lgslem1  16090