Theorem f1oeq3d 6859

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 6852	. 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 1537  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  resdif  6883  f1osng  6903  f1oresrab  7161  fveqf1o  7338  isoini2  7375  oacomf1o  8621  mapsnf1o  8997  domss2  9202  dif1enlem  9222  dif1enlemOLD  9223  infn0  9368  wemapwe  9766  oef1o  9767  cnfcomlem  9768  cnfcom3  9773  cnfcom3clem  9774  infxpenc  10087  infxpenc2lem1  10088  infxpenc2  10091  ackbij2lem2  10308  hsmexlem1  10495  fsumss  15773  fsumcnv  15821  fprodss  15996  fprodcnv  16031  pwssnf1o  17558  catcisolem  18177  equivestrcsetc  18221  yoniso  18355  gsumpropd  18716  gsumpropd2lem  18717  xpsmnd  18812  xpsgrp  19099  ghmqusker  19327  gsumval3lem1  19947  gsumval3lem2  19948  gsumcom2  20017  xpsrngd  20206  xpsringd  20355  rngqiprngim  21337  coe1mul2lem2  22292  scmatrngiso  22563  m2cpmrngiso  22785  cncfcnvcn  24971  isismt  28560  usgrf1oedg  29242  wlkiswwlks2lem5  29906  clwwlkvbij  30145  eupthres  30247  eupthp1  30248  cycpmconjvlem  33134  tocyccntz  33137  idomsubr  33276  dimkerim  33640  prodeq12sdv  36184  cbvsumdavw2  36261  cbvproddavw2  36262  poimirlem4  37584  poimirlem9  37589  rngoisoval  37937  frlmsnic  42495  sge0f1o  46303  nnfoctbdj  46377  3f1oss1  46990  f1oresf1o  47205  grimidvtxedg  47760  ushggricedg  47780  uhgrimisgrgric  47783