Theorem f1oeq3d 6765

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 6758	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  –1-1-onto→wf1o 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  resdif  6789  f1osng  6810  f1oresrab  7070  fveqf1o  7247  isoini2  7284  oacomf1o  8491  mapsnf1o  8878  domss2  9065  dif1enlem  9085  infn0  9203  wemapwe  9610  oef1o  9611  cnfcomlem  9612  cnfcom3  9617  cnfcom3clem  9618  infxpenc  9932  infxpenc2lem1  9933  infxpenc2  9936  ackbij2lem2  10153  hsmexlem1  10340  fsumss  15679  fsumcnv  15727  fprodss  15905  fprodcnv  15940  pwssnf1o  17454  catcisolem  18069  equivestrcsetc  18110  yoniso  18243  gsumpropd  18638  gsumpropd2lem  18639  xpsmnd  18737  xpsgrp  19027  ghmqusker  19254  gsumval3lem1  19872  gsumval3lem2  19873  gsumcom2  19942  xpsrngd  20152  xpsringd  20304  rngqiprngim  21298  coe1mul2lem2  22255  scmatrngiso  22520  m2cpmrngiso  22742  cncfcnvcn  24911  isismt  28621  usgrf1oedg  29295  wlkiswwlks2lem5  29960  clwwlkvbij  30202  eupthres  30304  eupthp1  30305  f1oeq3dd  32722  cycpmconjvlem  33223  tocyccntz  33226  idomsubr  33394  dimkerim  33820  prodeq12sdv  36455  cbvsumdavw2  36532  cbvproddavw2  36533  poimirlem4  38000  poimirlem9  38005  rngoisoval  38353  frlmsnic  43035  sge0f1o  46833  nnfoctbdj  46907  3f1oss1  47546  f1oresf1o  47761  grimidvtxedg  48384  ushggricedg  48426  uhgrimisgrgric  48430  isubgr3stgrlem3  48467  uptrlem1  49708  uptrar  49714  uptr2  49719  oduoppcciso  50064