Theorem f1oeq1 6791

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 6754	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6771	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6521	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6521	. 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 1540  –1-1→wf1 6511  –onto→wfo 6512  –1-1-onto→wf1o 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1oeq123d  6797  f1oeq1d  6798  f1ocnvb  6816  resin  6825  f1ovi  6842  f1oresrab  7102  fsn  7110  f1ounsn  7250  fveqf1o  7280  isoeq1  7295  f1oexbi  7907  oacomf1o  8532  mapsnd  8862  mapsnf1o3  8871  f1oen4g  8939  f1oen3g  8941  en0  8992  en0r  8994  ensn1  8995  en2sn  9015  en2prd  9022  xpcomf1o  9035  omf1o  9049  enfixsn  9055  domss2  9106  ssfiALT  9144  php3  9179  isinf  9214  isinfOLD  9215  oef1o  9658  cnfcom  9660  cnfcom3  9664  infxpenc  9978  ackbij2lem2  10199  ackbij2  10202  canthp1lem2  10613  pwfseqlem5  10623  seqf1olem2  14014  seqf1o  14015  hasheqf1oi  14323  hashf1rn  14324  hasheqf1od  14325  hashfacen  14426  wrd2f1tovbij  14933  s7f1o  14939  summo  15690  fsum  15693  ackbijnn  15801  prodmo  15909  fprod  15914  sadcaddlem  16434  unbenlem  16886  setcinv  18059  equivestrcsetc  18120  isgim  19201  symgval  19308  elsymgbas2  19310  symg1bas  19328  cayleyth  19352  gsumval3eu  19841  gsumval3lem1  19842  gsumval3lem2  19843  islmim  20976  uvcendim  21763  coe1mul2lem2  22161  mdet0f1o  22487  resinf1o  26452  efif1olem4  26461  logf1o  26480  relogf1o  26482  dvlog  26567  2lgslem1  27312  isismt  28468  nbusgrf1o1  29304  cusgrfilem3  29392  wwlksnextbij  29839  wlksnwwlknvbij  29845  clwwlkvbij  30049  hoif  31690  rabfodom  32441  fresf1o  32562  fpwrelmapffs  32664  fzo0pmtrlast  33056  pmtridf1o  33058  cycpmconjslem2  33119  1arithidomlem1  33513  1arithidom  33515  eulerpartlem1  34365  eulerpartgbij  34370  eulerpart  34380  derangenlem  35165  subfacp1lem2a  35174  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  subfacp1  35180  f1omptsn  37332  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem31  37652  isismty  37802  isrngoiso  37979  islaut  40084  ispautN  40100  aks6d1c2  42125  sticksstones4  42144  sticksstones20  42161  eldioph2lem1  42755  pwfi2f1o  43092  rfovcnvf1od  44000  clsneif1o  44100  neicvgf1o  44110  nregmodelf1o  45012  3f1oss1  47080  fundcmpsurbijinjpreimafv  47412  sprbisymrel  47504  prproropen  47513  grimidvtxedg  47889  grimcnv  47892  grimco  47893  isuspgrim0  47898  gricushgr  47921  ushggricedg  47931  uhgrimisgrgric  47935  isgrtri  47946  isubgr3stgrlem3  47971  isubgr3stgr  47978  isgrlim  47985  uspgrlim  47995  grlicref  48008  grlicsym  48009  grlictr  48011  uspgrbispr  48143  uspgrbisymrelALT  48147  1aryenef  48638  2aryenef  48649  rrx2xpreen  48712  thincciso  49446  thinccisod  49447