Theorem f1oeq1 6606

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 6572	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6588	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6364	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6364	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  –1-1→wf1 6354  –onto→wfo 6355  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  f1oeq123d  6612  f1ocnvb  6630  f1orescnv  6632  resin  6638  f1ovi  6655  f1osng  6657  f1oresrab  6891  fsn  6899  fveqf1o  7060  isoeq1  7072  f1oexbi  7635  oacomf1o  8193  mapsnd  8452  mapsnf1o3  8461  f1oen3g  8527  ensn1  8575  xpcomf1o  8608  omf1o  8622  enfixsn  8628  domss2  8678  php3  8705  isinf  8733  ssfi  8740  oef1o  9163  cnfcomlem  9164  cnfcom  9165  cnfcom2  9167  cnfcom3  9169  cnfcom3clem  9170  infxpenc  9446  infxpenc2lem2  9448  infxpenc2  9450  ackbij2lem2  9664  ackbij2  9667  canthp1lem2  10077  pwfseqlem5  10087  pwfseq  10088  seqf1olem2  13413  seqf1o  13414  hasheqf1oi  13715  hashf1rn  13716  hasheqf1od  13717  hashfacen  13815  wrd2f1tovbij  14326  summo  15076  fsum  15079  ackbijnn  15185  prodmo  15292  fprod  15297  bitsf1ocnv  15795  sadcaddlem  15808  unbenlem  16246  setcinv  17352  equivestrcsetc  17404  yonffthlem  17534  grplactcnv  18204  eqgen  18335  isgim  18404  symgval  18499  elsymgbas2  18503  symg1bas  18521  cayleyth  18545  gsumval3eu  19026  gsumval3lem1  19027  gsumval3lem2  19028  islmim  19836  coe1mul2lem2  20438  znunithash  20713  uvcendim  20993  mdet0f1o  21204  tgpconncompeqg  22722  resinf1o  25122  efif1olem4  25131  logf1o  25150  relogf1o  25152  dvlog  25236  2lgslem1  25972  isismt  26322  nbusgrf1o1  27154  cusgrfilem3  27241  wwlksnextbij  27682  wlksnwwlknvbij  27689  clwwlkvbij  27894  hoif  29533  rabfodom  30268  fresf1o  30378  fcobijfs  30461  fpwrelmapffs  30472  s2f1  30623  gsummpt2d  30689  pmtridf1o  30738  cycpmconjslem2  30799  indf1o  31285  eulerpartlem1  31627  eulerpartgbij  31632  eulerpart  31642  derangenlem  32420  subfacp1lem2a  32429  subfacp1lem3  32431  subfacp1lem5  32433  subfacp1lem6  32434  subfacp1  32435  f1omptsn  34620  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem29  34923  poimirlem31  34925  isismty  35081  ismrer1  35118  isrngoiso  35258  islaut  37221  ispautN  37237  hvmap1o  38901  eldioph2lem1  39364  pwfi2f1o  39703  rfovcnvf1od  40357  clsneif1o  40461  neicvgf1o  40471  f1oeq1d  41444  fundcmpsurbijinjpreimafv  43574  sprbisymrel  43668  prproropen  43677  isomgreqve  43997  isomushgr  43998  isomuspgrlem2  44005  isomgrsym  44008  isomgrtr  44011  ushrisomgr  44013  uspgrbispr  44033  uspgrbisymrelALT  44037  rrx2xpreen  44713