Theorem f1oeq1 6770

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 6733	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6750	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6507	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6507	. 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 1542  –1-1→wf1 6497  –onto→wfo 6498  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1oeq123d  6776  f1oeq1d  6777  f1ocnvb  6795  resin  6804  f1ovi  6822  f1oresrab  7082  fsn  7090  f1ounsn  7228  fveqf1o  7258  isoeq1  7273  f1oexbi  7880  oacomf1o  8502  mapsnd  8836  mapsnf1o3  8845  f1oen4g  8913  f1oen3g  8915  en0  8967  en0r  8969  ensn1  8970  en2sn  8990  en2prd  8996  xpcomf1o  9006  omf1o  9020  enfixsn  9026  domss2  9076  ssfiALT  9110  php3  9145  isinf  9177  oef1o  9619  cnfcom  9621  cnfcom3  9625  infxpenc  9940  ackbij2lem2  10161  ackbij2  10164  canthp1lem2  10576  pwfseqlem5  10586  seqf1olem2  13977  seqf1o  13978  hasheqf1oi  14286  hashf1rn  14287  hasheqf1od  14288  hashfacen  14389  wrd2f1tovbij  14895  s7f1o  14901  summo  15652  fsum  15655  ackbijnn  15763  prodmo  15871  fprod  15876  sadcaddlem  16396  unbenlem  16848  setcinv  18026  equivestrcsetc  18087  isgim  19203  symgval  19312  elsymgbas2  19314  symg1bas  19332  cayleyth  19356  gsumval3eu  19845  gsumval3lem1  19846  gsumval3lem2  19847  islmim  21026  uvcendim  21814  coe1mul2lem2  22222  mdet0f1o  22549  resinf1o  26513  efif1olem4  26522  logf1o  26541  relogf1o  26543  dvlog  26628  2lgslem1  27373  isismt  28618  nbusgrf1o1  29455  cusgrfilem3  29543  wwlksnextbij  29987  wlksnwwlknvbij  29993  clwwlkvbij  30200  hoif  31842  rabfodom  32592  fresf1o  32721  fpwrelmapffs  32824  fzo0pmtrlast  33186  pmtridf1o  33188  cycpmconjslem2  33249  1arithidomlem1  33628  1arithidom  33630  eulerpartlem1  34545  eulerpartgbij  34550  eulerpart  34560  derangenlem  35387  subfacp1lem2a  35396  subfacp1lem3  35398  subfacp1lem5  35400  subfacp1lem6  35401  subfacp1  35402  f1omptsn  37592  poimirlem3  37874  poimirlem4  37875  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem9  37880  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem29  37900  poimirlem31  37902  isismty  38052  isrngoiso  38229  islaut  40459  ispautN  40475  aks6d1c2  42500  sticksstones4  42519  sticksstones20  42536  eldioph2lem1  43117  pwfi2f1o  43453  rfovcnvf1od  44360  clsneif1o  44460  neicvgf1o  44470  nregmodelf1o  45371  3f1oss1  47435  fundcmpsurbijinjpreimafv  47767  sprbisymrel  47859  prproropen  47868  grimidvtxedg  48245  grimcnv  48248  grimco  48249  isuspgrim0  48254  gricushgr  48277  ushggricedg  48287  uhgrimisgrgric  48291  isgrtri  48303  isubgr3stgrlem3  48328  isubgr3stgr  48335  isgrlim  48342  uspgrlim  48352  grlicref  48372  grlicsym  48373  grlictr  48375  uspgrbispr  48511  uspgrbisymrelALT  48515  1aryenef  49005  2aryenef  49016  rrx2xpreen  49079  thincciso  49812  thinccisod  49813