Theorem f1oeq3d 6772

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 6765	. 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 1542  –1-1-onto→wf1o 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  resdif  6796  f1osng  6817  f1oresrab  7075  fveqf1o  7251  isoini2  7288  oacomf1o  8494  mapsnf1o  8881  domss2  9068  dif1enlem  9088  infn0  9206  wemapwe  9612  oef1o  9613  cnfcomlem  9614  cnfcom3  9619  cnfcom3clem  9620  infxpenc  9934  infxpenc2lem1  9935  infxpenc2  9938  ackbij2lem2  10155  hsmexlem1  10342  fsumss  15681  fsumcnv  15729  fprodss  15907  fprodcnv  15942  pwssnf1o  17456  catcisolem  18071  equivestrcsetc  18112  yoniso  18245  gsumpropd  18640  gsumpropd2lem  18641  xpsmnd  18739  xpsgrp  19029  ghmqusker  19256  gsumval3lem1  19874  gsumval3lem2  19875  gsumcom2  19944  xpsrngd  20154  xpsringd  20306  rngqiprngim  21297  coe1mul2lem2  22246  scmatrngiso  22514  m2cpmrngiso  22736  cncfcnvcn  24905  isismt  28619  usgrf1oedg  29293  wlkiswwlks2lem5  29959  clwwlkvbij  30201  eupthres  30303  eupthp1  30304  f1oeq3dd  32720  cycpmconjvlem  33220  tocyccntz  33223  idomsubr  33388  dimkerim  33790  prodeq12sdv  36419  cbvsumdavw2  36496  cbvproddavw2  36497  poimirlem4  37962  poimirlem9  37967  rngoisoval  38315  frlmsnic  43002  sge0f1o  46831  nnfoctbdj  46905  3f1oss1  47538  f1oresf1o  47753  grimidvtxedg  48376  ushggricedg  48418  uhgrimisgrgric  48422  isubgr3stgrlem3  48459  uptrlem1  49700  uptrar  49706  uptr2  49711  oduoppcciso  50056