Theorem f1oeq3d 6826

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  resdif  6851  f1osng  6872  f1oresrab  7133  fveqf1o  7314  isoini2  7351  oacomf1o  8580  mapsnf1o  8974  domss2  9162  dif1enlem  9182  infn0  9301  wemapwe  9705  oef1o  9706  cnfcomlem  9707  cnfcom3  9712  cnfcom3clem  9713  infxpenc  10104  infxpenc2lem1  10105  infxpenc2  10108  ackbij2lem2  10324  hsmexlem1  10511  fsumss  15900  fsumcnv  15948  fprodss  16124  fprodcnv  16159  pwssnf1o  17679  catcisolem  18294  equivestrcsetc  18335  yoniso  18468  gsumpropd  18876  gsumpropd2lem  18877  xpsmnd  18980  xpsgrp  19278  ghmqusker  19510  gsumval3lem1  20128  gsumval3lem2  20129  gsumcom2  20198  xpsrngd  20410  xpsringd  20571  rngqiprngim  21609  coe1mul2lem2  22596  scmatrngiso  22860  m2cpmrngiso  23085  cncfcnvcn  25255  isismt  29006  usgrf1oedg  29797  wlkiswwlks2lem5  30471  clwwlkvbij  30713  eupthres  30825  eupthp1  30826  f1oeq3dd  33274  cycpmconjvlem  33752  tocyccntz  33755  idomsubr  33921  dimkerim  34309  prodeq12sdv  37103  cbvsumdavw2  37180  cbvproddavw2  37181  poimirlem4  38651  poimirlem9  38656  rngoisoval  39020  frlmsnic  43713  sge0f1o  47500  nnfoctbdj  47574  3f1oss1  48253  f1oresf1o  48468  grimidvtxedg  49091  ushggricedg  49133  uhgrimisgrgric  49137  isubgr3stgrlem3  49174  uptrlem1  50434  uptrar  50440  uptr2  50445  oduoppcciso  50812