Theorem f1oeq1 6768

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 6731	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6748	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6505	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6505	. 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 6495  –onto→wfo 6496  –1-1-onto→wf1o 6497

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1oeq123d  6774  f1oeq1d  6775  f1ocnvb  6793  resin  6802  f1ovi  6820  f1oresrab  7080  fsn  7088  f1ounsn  7227  fveqf1o  7257  isoeq1  7272  f1oexbi  7879  oacomf1o  8500  mapsnd  8834  mapsnf1o3  8843  f1oen4g  8911  f1oen3g  8913  en0  8965  en0r  8967  ensn1  8968  en2sn  8988  en2prd  8994  xpcomf1o  9004  omf1o  9018  enfixsn  9024  domss2  9074  ssfiALT  9108  php3  9143  isinf  9175  oef1o  9619  cnfcom  9621  cnfcom3  9625  infxpenc  9940  ackbij2lem2  10161  ackbij2  10164  canthp1lem2  10576  pwfseqlem5  10586  seqf1olem2  14004  seqf1o  14005  hasheqf1oi  14313  hashf1rn  14314  hasheqf1od  14315  hashfacen  14416  wrd2f1tovbij  14922  s7f1o  14928  summo  15679  fsum  15682  ackbijnn  15793  prodmo  15901  fprod  15906  sadcaddlem  16426  unbenlem  16879  setcinv  18057  equivestrcsetc  18118  isgim  19237  symgval  19346  elsymgbas2  19348  symg1bas  19366  cayleyth  19390  gsumval3eu  19879  gsumval3lem1  19880  gsumval3lem2  19881  islmim  21057  uvcendim  21827  coe1mul2lem2  22233  mdet0f1o  22558  resinf1o  26500  efif1olem4  26509  logf1o  26528  relogf1o  26530  dvlog  26615  2lgslem1  27357  isismt  28602  nbusgrf1o1  29439  cusgrfilem3  29526  wwlksnextbij  29970  wlksnwwlknvbij  29976  clwwlkvbij  30183  hoif  31825  rabfodom  32575  fresf1o  32704  fpwrelmapffs  32807  fzo0pmtrlast  33153  pmtridf1o  33155  cycpmconjslem2  33216  1arithidomlem1  33595  1arithidom  33597  eulerpartlem1  34511  eulerpartgbij  34516  eulerpart  34526  derangenlem  35353  subfacp1lem2a  35362  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  subfacp1  35368  f1omptsn  37653  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  isismty  38122  isrngoiso  38299  islaut  40529  ispautN  40545  aks6d1c2  42569  sticksstones4  42588  sticksstones20  42605  eldioph2lem1  43192  pwfi2f1o  43524  rfovcnvf1od  44431  clsneif1o  44531  neicvgf1o  44541  nregmodelf1o  45442  3f1oss1  47523  fundcmpsurbijinjpreimafv  47867  sprbisymrel  47959  prproropen  47968  grimidvtxedg  48361  grimcnv  48364  grimco  48365  isuspgrim0  48370  gricushgr  48393  ushggricedg  48403  uhgrimisgrgric  48407  isgrtri  48419  isubgr3stgrlem3  48444  isubgr3stgr  48451  isgrlim  48458  uspgrlim  48468  grlicref  48488  grlicsym  48489  grlictr  48491  uspgrbispr  48627  uspgrbisymrelALT  48631  1aryenef  49121  2aryenef  49132  rrx2xpreen  49195  thincciso  49928  thinccisod  49929