Theorem f1oeq1 6040

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 6009	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6024	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 743	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 5811	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 5811	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 302	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811

This theorem is referenced by:  f1oeq123d  6046  f1ocnvb  6063  f1orescnv  6065  resin  6071  f1ovi  6087  f1osng  6089  f1oresrab  6302  fsn  6308  fveqf1o  6457  isoeq1  6467  f1oexbi  7009  oacomf1o  7532  mapsn  7785  mapsnf1o3  7792  f1oen3g  7857  ensn1  7906  xpcomf1o  7934  omf1o  7948  enfixsn  7954  domss2  8004  php3  8031  isinf  8058  ssfi  8065  oef1o  8478  cnfcomlem  8479  cnfcom  8480  cnfcom2  8482  cnfcom3  8484  cnfcom3clem  8485  infxpenc  8724  infxpenc2lem2  8726  infxpenc2  8728  ackbij2lem2  8945  ackbij2  8948  canthp1lem2  9354  pwfseqlem5  9364  pwfseq  9365  seqf1olem2  12703  seqf1o  12704  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashf1rn  13004  hashf1rnOLD  13005  hasheqf1od  13006  hashfacen  13095  wrd2f1tovbij  13551  summo  14295  fsum  14298  ackbijnn  14399  prodmo  14505  fprod  14510  bitsf1ocnv  15004  sadcaddlem  15017  unbenlem  15450  setcinv  16563  equivestrcsetc  16615  yonffthlem  16745  grplactcnv  17341  eqgen  17470  isgim  17527  elsymgbas2  17624  symg1bas  17639  cayleyth  17658  gsumval3eu  18128  gsumval3lem1  18129  gsumval3lem2  18130  islmim  18883  coe1mul2lem2  19459  znunithash  19732  uvcendim  20005  mdet0f1o  20218  tgpconcompeqg  21725  resinf1o  24086  efif1olem4  24095  logf1o  24115  relogf1o  24117  dvlog  24197  2lgslem1  24919  isismt  25229  nbgraf1o0  25975  cusgrafilem3  26009  wlknwwlknbij2  26242  wlkiswwlkbij2  26249  wwlkextbij  26261  wlknwwlknvbij  26268  clwwlkbij  26327  clwwlkvbij  26329  iseupa  26492  eupares  26502  eupap1  26503  frgrancvvdeqlem9  26568  numclwlk1lem2  26624  hoif  27997  rabfodom  28728  fresf1o  28815  fcobijfs  28889  fpwrelmapffs  28897  gsummpt2d  29112  indf1o  29413  eulerpartlem1  29756  eulerpartgbij  29761  eulerpart  29771  derangenlem  30407  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  subfacp1  30422  f1omptsn  32360  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  isismty  32770  ismrer1  32807  isrngoiso  32947  islaut  34387  ispautN  34403  hvmap1o  36070  eldioph2lem1  36341  pwfi2f1o  36684  rfovcnvf1od  37318  clsneif1o  37422  neicvgf1o  37432  f1oeq1d  38358  mapsnd  38383  nbusgrf1o1  40598  cusgrfilem3  40673  1wlkisowwlkupgr  41077  wlknwwlksnbij2  41089  wlkwwlkbij2  41096  wwlksnextbij  41108  wlksnwwlknvbij  41114  clwwlksbij  41227  clwwlksvbij  41229  av-numclwlk1lem2  41527