Theorem f1oeq1 6760

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

Assertion

Ref	Expression
f1oeq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Proof of Theorem f1oeq1

Step	Hyp	Ref	Expression
1		f1eq1 6723	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6740	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6497	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6497	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  –1-1→wf1 6487  –onto→wfo 6488  –1-1-onto→wf1o 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1oeq123d  6766  f1oeq1d  6767  f1ocnvb  6785  resin  6794  f1ovi  6812  f1oresrab  7070  fsn  7078  f1ounsn  7216  fveqf1o  7246  isoeq1  7261  f1oexbi  7868  oacomf1o  8490  mapsnd  8822  mapsnf1o3  8831  f1oen4g  8899  f1oen3g  8901  en0  8953  en0r  8955  ensn1  8956  en2sn  8976  en2prd  8982  xpcomf1o  8992  omf1o  9006  enfixsn  9012  domss2  9062  ssfiALT  9096  php3  9131  isinf  9163  oef1o  9605  cnfcom  9607  cnfcom3  9611  infxpenc  9926  ackbij2lem2  10147  ackbij2  10150  canthp1lem2  10562  pwfseqlem5  10572  seqf1olem2  13963  seqf1o  13964  hasheqf1oi  14272  hashf1rn  14273  hasheqf1od  14274  hashfacen  14375  wrd2f1tovbij  14881  s7f1o  14887  summo  15638  fsum  15641  ackbijnn  15749  prodmo  15857  fprod  15862  sadcaddlem  16382  unbenlem  16834  setcinv  18012  equivestrcsetc  18073  isgim  19189  symgval  19298  elsymgbas2  19300  symg1bas  19318  cayleyth  19342  gsumval3eu  19831  gsumval3lem1  19832  gsumval3lem2  19833  islmim  21012  uvcendim  21800  coe1mul2lem2  22208  mdet0f1o  22535  resinf1o  26499  efif1olem4  26508  logf1o  26527  relogf1o  26529  dvlog  26614  2lgslem1  27359  isismt  28555  nbusgrf1o1  29392  cusgrfilem3  29480  wwlksnextbij  29924  wlksnwwlknvbij  29930  clwwlkvbij  30137  hoif  31778  rabfodom  32529  fresf1o  32658  fpwrelmapffs  32762  fzo0pmtrlast  33123  pmtridf1o  33125  cycpmconjslem2  33186  1arithidomlem1  33565  1arithidom  33567  eulerpartlem1  34473  eulerpartgbij  34478  eulerpart  34488  derangenlem  35314  subfacp1lem2a  35323  subfacp1lem3  35325  subfacp1lem5  35327  subfacp1lem6  35328  subfacp1  35329  f1omptsn  37481  poimirlem3  37763  poimirlem4  37764  poimirlem5  37765  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem9  37769  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  poimirlem29  37789  poimirlem31  37791  isismty  37941  isrngoiso  38118  islaut  40282  ispautN  40298  aks6d1c2  42323  sticksstones4  42342  sticksstones20  42359  eldioph2lem1  42944  pwfi2f1o  43280  rfovcnvf1od  44187  clsneif1o  44287  neicvgf1o  44297  nregmodelf1o  45198  3f1oss1  47263  fundcmpsurbijinjpreimafv  47595  sprbisymrel  47687  prproropen  47696  grimidvtxedg  48073  grimcnv  48076  grimco  48077  isuspgrim0  48082  gricushgr  48105  ushggricedg  48115  uhgrimisgrgric  48119  isgrtri  48131  isubgr3stgrlem3  48156  isubgr3stgr  48163  isgrlim  48170  uspgrlim  48180  grlicref  48200  grlicsym  48201  grlictr  48203  uspgrbispr  48339  uspgrbisymrelALT  48343  1aryenef  48833  2aryenef  48844  rrx2xpreen  48907  thincciso  49640  thinccisod  49641