Theorem f1oeq1 6805

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  –1-1→wf1 6530  –onto→wfo 6531  –1-1-onto→wf1o 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1oeq123d  6811  f1oeq1d  6812  f1ocnvb  6831  resin  6840  f1ovi  6858  f1oresrab  7121  fsn  7129  f1ounsn  7273  fveqf1o  7303  isoeq1  7318  f1oexbi  7925  oacomf1o  8552  mapsnd  8893  mapsnf1o3  8902  f1oen4g  8970  f1oen3g  8972  en0  9024  en0r  9026  ensn1  9027  en2sn  9048  en2prd  9054  xpcomf1o  9064  omf1o  9078  enfixsn  9084  domss2  9134  ssfiALT  9168  php3  9203  isinf  9235  oef1o  9677  cnfcom  9679  cnfcom3  9683  infxpenc  10021  ackbij2lem2  10241  ackbij2  10244  canthp1lem2  10662  pwfseqlem5  10672  seqf1olem2  14106  seqf1o  14107  hasheqf1oi  14415  hashf1rn  14416  hasheqf1od  14417  hashfacen  14519  wrd2f1tovbij  15033  s7f1o  15039  summo  15803  fsum  15806  ackbijnn  15917  prodmo  16023  fprod  16028  sadcaddlem  16547  unbenlem  17000  setcinv  18179  equivestrcsetc  18240  isgim  19389  symgval  19498  elsymgbas2  19500  symg1bas  19518  cayleyth  19542  gsumval3eu  20031  gsumval3lem1  20032  gsumval3lem2  20033  rimval  20641  islmim  21246  uvcendim  22060  coe1mul2lem2  22494  mdet0f1o  22815  resinf1o  26773  efif1olem4  26782  logf1o  26801  relogf1o  26803  dvlog  26888  2lgslem1  27630  isismt  28876  nbusgrf1o1  29830  cusgrfilem3  29917  wwlksnextbij  30370  wlksnwwlknvbij  30376  clwwlkvbij  30583  hoif  32235  rabfodom  32980  fresf1o  33104  fpwrelmapffs  33205  fzo0pmtrlast  33532  pmtridf1o  33534  cycpmconjslem2  33595  1arithidomlem1  33945  1arithidom  33947  eulerpartlem1  34878  eulerpartgbij  34883  eulerpart  34893  derangenlem  35750  subfacp1lem2a  35759  subfacp1lem3  35761  subfacp1lem5  35763  subfacp1lem6  35764  subfacp1  35765  f1omptsn  38091  poimirlem3  38372  poimirlem4  38373  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem9  38378  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem29  38398  poimirlem31  38400  isismty  38551  isrngoiso  38728  islaut  40956  ispautN  40972  aks6d1c2  42996  sticksstones4  43015  sticksstones20  43032  eldioph2lem1  43605  pwfi2f1o  43937  rfovcnvf1od  44844  clsneif1o  44944  neicvgf1o  44954  nregmodelf1o  45838  3f1oss1  47963  fundcmpsurbijinjpreimafv  48307  sprbisymrel  48399  prproropen  48408  grimidvtxedg  48801  grimcnv  48804  grimco  48805  isuspgrim0  48810  gricushgr  48833  ushggricedg  48843  uhgrimisgrgric  48847  isgrtri  48859  isubgr3stgrlem3  48884  isubgr3stgr  48891  isgrlim  48898  uspgrlim  48908  grlicref  48928  grlicsym  48929  grlictr  48931  uspgrbispr  49067  uspgrbisymrelALT  49071  1aryenef  49575  2aryenef  49586  rrx2xpreen  49649  thincciso  50379  thinccisod  50380