Theorem f1oeq3d 6771

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq3d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
f1oeq3d	⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Proof of Theorem f1oeq3d

Step	Hyp	Ref	Expression
1		f1oeq3d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq3 6764	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  –1-1-onto→wf1o 6491

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  resdif  6795  f1osng  6816  f1oresrab  7072  fveqf1o  7248  isoini2  7285  oacomf1o  8492  mapsnf1o  8877  domss2  9064  dif1enlem  9084  infn0  9202  wemapwe  9606  oef1o  9607  cnfcomlem  9608  cnfcom3  9613  cnfcom3clem  9614  infxpenc  9928  infxpenc2lem1  9929  infxpenc2  9932  ackbij2lem2  10149  hsmexlem1  10336  fsumss  15648  fsumcnv  15696  fprodss  15871  fprodcnv  15906  pwssnf1o  17419  catcisolem  18034  equivestrcsetc  18075  yoniso  18208  gsumpropd  18603  gsumpropd2lem  18604  xpsmnd  18702  xpsgrp  18989  ghmqusker  19216  gsumval3lem1  19834  gsumval3lem2  19835  gsumcom2  19904  xpsrngd  20114  xpsringd  20268  rngqiprngim  21259  coe1mul2lem2  22210  scmatrngiso  22480  m2cpmrngiso  22702  cncfcnvcn  24875  isismt  28606  usgrf1oedg  29280  wlkiswwlks2lem5  29946  clwwlkvbij  30188  eupthres  30290  eupthp1  30291  f1oeq3dd  32707  cycpmconjvlem  33223  tocyccntz  33226  idomsubr  33391  dimkerim  33784  prodeq12sdv  36412  cbvsumdavw2  36489  cbvproddavw2  36490  poimirlem4  37825  poimirlem9  37830  rngoisoval  38178  frlmsnic  42795  sge0f1o  46626  nnfoctbdj  46700  3f1oss1  47321  f1oresf1o  47536  grimidvtxedg  48131  ushggricedg  48173  uhgrimisgrgric  48177  isubgr3stgrlem3  48214  uptrlem1  49455  uptrar  49461  uptr2  49466  oduoppcciso  49811