Theorem f1oeq1 6809

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 6770	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6789	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6544	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6544	. 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 1567  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  f1oeq123d  6815  f1oeq1d  6816  f1ocnvb  6835  resin  6844  f1ovi  6862  f1oresrab  7124  fsn  7132  f1ounsn  7271  fveqf1o  7301  isoeq1  7316  f1oexbi  7924  oacomf1o  8549  mapsnd  8883  mapsnf1o3  8892  f1oen4g  8960  f1oen3g  8962  en0  9014  en0r  9016  ensn1  9017  en2sn  9037  en2prd  9043  xpcomf1o  9053  omf1o  9067  enfixsn  9073  domss2  9123  ssfiALT  9157  php3  9192  isinf  9224  oef1o  9666  cnfcom  9668  cnfcom3  9672  infxpenc  10001  ackbij2lem2  10221  ackbij2  10224  canthp1lem2  10637  pwfseqlem5  10647  seqf1olem2  14077  seqf1o  14078  hasheqf1oi  14386  hashf1rn  14387  hasheqf1od  14388  hashfacen  14490  wrd2f1tovbij  14996  s7f1o  15002  summo  15767  fsum  15770  ackbijnn  15881  prodmo  15989  fprod  15994  sadcaddlem  16514  unbenlem  16967  setcinv  18146  equivestrcsetc  18207  isgim  19331  symgval  19440  elsymgbas2  19442  symg1bas  19460  cayleyth  19484  gsumval3eu  19973  gsumval3lem1  19974  gsumval3lem2  19975  islmim  21160  uvcendim  21965  coe1mul2lem2  22397  mdet0f1o  22718  resinf1o  26666  efif1olem4  26675  logf1o  26694  relogf1o  26696  dvlog  26781  2lgslem1  27523  isismt  28768  nbusgrf1o1  29660  cusgrfilem3  29747  wwlksnextbij  30191  wlksnwwlknvbij  30197  clwwlkvbij  30404  hoif  32046  rabfodom  32791  fresf1o  32916  fpwrelmapffs  33019  fzo0pmtrlast  33352  pmtridf1o  33354  cycpmconjslem2  33415  1arithidomlem1  33769  1arithidom  33771  eulerpartlem1  34701  eulerpartgbij  34706  eulerpart  34716  derangenlem  35561  subfacp1lem2a  35570  subfacp1lem3  35572  subfacp1lem5  35574  subfacp1lem6  35575  subfacp1  35576  f1omptsn  37870  poimirlem3  38161  poimirlem4  38162  poimirlem5  38163  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem9  38167  poimirlem10  38168  poimirlem11  38169  poimirlem12  38170  poimirlem13  38171  poimirlem14  38172  poimirlem15  38173  poimirlem16  38174  poimirlem17  38175  poimirlem18  38176  poimirlem19  38177  poimirlem20  38178  poimirlem21  38179  poimirlem22  38180  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  poimirlem29  38187  poimirlem31  38189  isismty  38339  isrngoiso  38516  islaut  40746  ispautN  40762  aks6d1c2  42786  sticksstones4  42805  sticksstones20  42822  eldioph2lem1  43382  pwfi2f1o  43714  rfovcnvf1od  44621  clsneif1o  44721  neicvgf1o  44731  nregmodelf1o  45615  3f1oss1  47700  fundcmpsurbijinjpreimafv  48044  sprbisymrel  48136  prproropen  48145  grimidvtxedg  48538  grimcnv  48541  grimco  48542  isuspgrim0  48547  gricushgr  48570  ushggricedg  48580  uhgrimisgrgric  48584  isgrtri  48596  isubgr3stgrlem3  48621  isubgr3stgr  48628  isgrlim  48635  uspgrlim  48645  grlicref  48665  grlicsym  48666  grlictr  48668  uspgrbispr  48804  uspgrbisymrelALT  48808  1aryenef  49309  2aryenef  49320  rrx2xpreen  49383  thincciso  50115  thinccisod  50116