Theorem f1oeq3d 6761

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 6754	. 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 1540  –1-1-onto→wf1o 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  resdif  6785  f1osng  6805  f1oresrab  7061  fveqf1o  7239  isoini2  7276  oacomf1o  8483  mapsnf1o  8866  domss2  9053  dif1enlem  9073  infn0  9191  wemapwe  9593  oef1o  9594  cnfcomlem  9595  cnfcom3  9600  cnfcom3clem  9601  infxpenc  9912  infxpenc2lem1  9913  infxpenc2  9916  ackbij2lem2  10133  hsmexlem1  10320  fsumss  15632  fsumcnv  15680  fprodss  15855  fprodcnv  15890  pwssnf1o  17402  catcisolem  18017  equivestrcsetc  18058  yoniso  18191  gsumpropd  18552  gsumpropd2lem  18553  xpsmnd  18651  xpsgrp  18938  ghmqusker  19166  gsumval3lem1  19784  gsumval3lem2  19785  gsumcom2  19854  xpsrngd  20064  xpsringd  20217  rngqiprngim  21211  coe1mul2lem2  22152  scmatrngiso  22421  m2cpmrngiso  22643  cncfcnvcn  24817  isismt  28479  usgrf1oedg  29152  wlkiswwlks2lem5  29818  clwwlkvbij  30057  eupthres  30159  eupthp1  30160  f1oeq3dd  32572  cycpmconjvlem  33083  tocyccntz  33086  idomsubr  33248  dimkerim  33594  prodeq12sdv  36192  cbvsumdavw2  36269  cbvproddavw2  36270  poimirlem4  37604  poimirlem9  37609  rngoisoval  37957  frlmsnic  42513  sge0f1o  46363  nnfoctbdj  46437  3f1oss1  47059  f1oresf1o  47274  grimidvtxedg  47869  ushggricedg  47911  uhgrimisgrgric  47915  isubgr3stgrlem3  47952  uptrlem1  49195  uptrar  49201  uptr2  49206  oduoppcciso  49551