Theorem f1oeq1 6755

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 6718	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6735	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 638	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6492	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6492	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 315	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  –1-1→wf1 6482  –onto→wfo 6483  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1oeq123d  6761  f1oeq1d  6762  f1ocnvb  6780  resin  6789  f1ovi  6807  f1oresrab  7069  fsn  7077  f1ounsn  7216  fveqf1o  7246  isoeq1  7261  f1oexbi  7868  oacomf1o  8490  mapsnd  8824  mapsnf1o3  8833  f1oen4g  8901  f1oen3g  8903  en0  8955  en0r  8957  ensn1  8958  en2sn  8978  en2prd  8984  xpcomf1o  8994  omf1o  9008  enfixsn  9014  domss2  9064  ssfiALT  9098  php3  9133  isinf  9165  oef1o  9610  cnfcom  9612  cnfcom3  9616  infxpenc  9931  ackbij2lem2  10152  ackbij2  10155  canthp1lem2  10567  pwfseqlem5  10577  seqf1olem2  13995  seqf1o  13996  hasheqf1oi  14304  hashf1rn  14305  hasheqf1od  14306  hashfacen  14407  wrd2f1tovbij  14913  s7f1o  14919  summo  15670  fsum  15673  ackbijnn  15784  prodmo  15892  fprod  15897  sadcaddlem  16417  unbenlem  16870  setcinv  18048  equivestrcsetc  18109  isgim  19228  symgval  19337  elsymgbas2  19339  symg1bas  19357  cayleyth  19381  gsumval3eu  19870  gsumval3lem1  19871  gsumval3lem2  19872  islmim  21052  uvcendim  21822  coe1mul2lem2  22254  mdet0f1o  22576  resinf1o  26518  efif1olem4  26527  logf1o  26546  relogf1o  26548  dvlog  26633  2lgslem1  27375  isismt  28620  nbusgrf1o1  29457  cusgrfilem3  29544  wwlksnextbij  29988  wlksnwwlknvbij  29994  clwwlkvbij  30201  hoif  31843  rabfodom  32593  fresf1o  32723  fpwrelmapffs  32826  fzo0pmtrlast  33173  pmtridf1o  33175  cycpmconjslem2  33236  1arithidomlem1  33618  1arithidom  33620  eulerpartlem1  34551  eulerpartgbij  34556  eulerpart  34566  derangenlem  35399  subfacp1lem2a  35408  subfacp1lem3  35410  subfacp1lem5  35412  subfacp1lem6  35413  subfacp1  35414  f1omptsn  37699  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem9  37996  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem29  38016  poimirlem31  38018  isismty  38168  isrngoiso  38345  islaut  40575  ispautN  40591  aks6d1c2  42615  sticksstones4  42634  sticksstones20  42651  eldioph2lem1  43209  pwfi2f1o  43541  rfovcnvf1od  44448  clsneif1o  44548  neicvgf1o  44558  nregmodelf1o  45459  3f1oss1  47538  fundcmpsurbijinjpreimafv  47882  sprbisymrel  47974  prproropen  47983  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  gricushgr  48408  ushggricedg  48418  uhgrimisgrgric  48422  isgrtri  48434  isubgr3stgrlem3  48459  isubgr3stgr  48466  isgrlim  48473  uspgrlim  48483  grlicref  48503  grlicsym  48504  grlictr  48506  uspgrbispr  48642  uspgrbisymrelALT  48646  1aryenef  49136  2aryenef  49147  rrx2xpreen  49210  thincciso  49943  thinccisod  49944