Theorem f1oeq3d 6820

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 6813	. 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 6535

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  resdif  6844  f1osng  6864  f1oresrab  7122  fveqf1o  7300  isoini2  7337  oacomf1o  8582  mapsnf1o  8958  domss2  9155  dif1enlem  9175  dif1enlemOLD  9176  infn0  9317  wemapwe  9716  oef1o  9717  cnfcomlem  9718  cnfcom3  9723  cnfcom3clem  9724  infxpenc  10037  infxpenc2lem1  10038  infxpenc2  10041  ackbij2lem2  10258  hsmexlem1  10445  fsumss  15746  fsumcnv  15794  fprodss  15969  fprodcnv  16004  pwssnf1o  17517  catcisolem  18128  equivestrcsetc  18169  yoniso  18302  gsumpropd  18661  gsumpropd2lem  18662  xpsmnd  18760  xpsgrp  19047  ghmqusker  19275  gsumval3lem1  19891  gsumval3lem2  19892  gsumcom2  19961  xpsrngd  20144  xpsringd  20297  rngqiprngim  21270  coe1mul2lem2  22210  scmatrngiso  22479  m2cpmrngiso  22701  cncfcnvcn  24875  isismt  28518  usgrf1oedg  29191  wlkiswwlks2lem5  29860  clwwlkvbij  30099  eupthres  30201  eupthp1  30202  cycpmconjvlem  33157  tocyccntz  33160  idomsubr  33308  dimkerim  33672  prodeq12sdv  36241  cbvsumdavw2  36318  cbvproddavw2  36319  poimirlem4  37653  poimirlem9  37658  rngoisoval  38006  frlmsnic  42530  sge0f1o  46378  nnfoctbdj  46452  3f1oss1  47071  f1oresf1o  47286  grimidvtxedg  47865  ushggricedg  47907  uhgrimisgrgric  47911  isubgr3stgrlem3  47947  oduoppcciso  49410