Theorem f1oeq1 6808

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 6769	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6788	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6543	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6543	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1oeq123d  6814  f1oeq1d  6815  f1ocnvb  6834  resin  6843  f1ovi  6861  f1oresrab  7123  fsn  7131  f1ounsn  7270  fveqf1o  7300  isoeq1  7315  f1oexbi  7921  oacomf1o  8546  mapsnd  8880  mapsnf1o3  8889  f1oen4g  8957  f1oen3g  8959  en0  9011  en0r  9013  ensn1  9014  en2sn  9034  en2prd  9040  xpcomf1o  9050  omf1o  9064  enfixsn  9070  domss2  9120  ssfiALT  9154  php3  9189  isinf  9221  oef1o  9663  cnfcom  9665  cnfcom3  9669  infxpenc  9998  ackbij2lem2  10218  ackbij2  10221  canthp1lem2  10633  pwfseqlem5  10643  seqf1olem2  14074  seqf1o  14075  hasheqf1oi  14383  hashf1rn  14384  hasheqf1od  14385  hashfacen  14487  wrd2f1tovbij  14993  s7f1o  14999  summo  15764  fsum  15767  ackbijnn  15878  prodmo  15986  fprod  15991  sadcaddlem  16510  unbenlem  16963  setcinv  18142  equivestrcsetc  18203  isgim  19327  symgval  19436  elsymgbas2  19438  symg1bas  19456  cayleyth  19480  gsumval3eu  19969  gsumval3lem1  19970  gsumval3lem2  19971  rimval  20578  islmim  21183  uvcendim  21997  coe1mul2lem2  22429  mdet0f1o  22750  resinf1o  26701  efif1olem4  26710  logf1o  26729  relogf1o  26731  dvlog  26816  2lgslem1  27558  isismt  28803  nbusgrf1o1  29720  cusgrfilem3  29807  wwlksnextbij  30251  wlksnwwlknvbij  30257  clwwlkvbij  30464  hoif  32106  rabfodom  32851  fresf1o  32976  fpwrelmapffs  33079  fzo0pmtrlast  33412  pmtridf1o  33414  cycpmconjslem2  33475  1arithidomlem1  33825  1arithidom  33827  eulerpartlem1  34757  eulerpartgbij  34762  eulerpart  34772  derangenlem  35663  subfacp1lem2a  35672  subfacp1lem3  35674  subfacp1lem5  35676  subfacp1lem6  35677  subfacp1  35678  f1omptsn  37983  poimirlem3  38274  poimirlem4  38275  poimirlem5  38276  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem9  38280  poimirlem10  38281  poimirlem11  38282  poimirlem12  38283  poimirlem13  38284  poimirlem14  38285  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  poimirlem29  38300  poimirlem31  38302  isismty  38452  isrngoiso  38629  islaut  40857  ispautN  40873  aks6d1c2  42897  sticksstones4  42916  sticksstones20  42933  eldioph2lem1  43491  pwfi2f1o  43823  rfovcnvf1od  44730  clsneif1o  44830  neicvgf1o  44840  nregmodelf1o  45724  3f1oss1  47812  fundcmpsurbijinjpreimafv  48156  sprbisymrel  48248  prproropen  48257  grimidvtxedg  48650  grimcnv  48653  grimco  48654  isuspgrim0  48659  gricushgr  48682  ushggricedg  48692  uhgrimisgrgric  48696  isgrtri  48708  isubgr3stgrlem3  48733  isubgr3stgr  48740  isgrlim  48747  uspgrlim  48757  grlicref  48777  grlicsym  48778  grlictr  48780  uspgrbispr  48916  uspgrbisymrelALT  48920  1aryenef  49425  2aryenef  49436  rrx2xpreen  49499  thincciso  50231  thinccisod  50232