Theorem f1oeq3d 6817

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  –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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  resdif  6842  f1osng  6863  f1oresrab  7123  fveqf1o  7300  isoini2  7337  oacomf1o  8546  mapsnf1o  8933  domss2  9120  dif1enlem  9140  infn0  9258  wemapwe  9662  oef1o  9663  cnfcomlem  9664  cnfcom3  9669  cnfcom3clem  9670  infxpenc  9998  infxpenc2lem1  9999  infxpenc2  10002  ackbij2lem2  10218  hsmexlem1  10405  fsumss  15772  fsumcnv  15820  fprodss  15998  fprodcnv  16033  pwssnf1o  17547  catcisolem  18162  equivestrcsetc  18203  yoniso  18336  gsumpropd  18731  gsumpropd2lem  18732  xpsmnd  18830  xpsgrp  19120  ghmqusker  19352  gsumval3lem1  19970  gsumval3lem2  19971  gsumcom2  20040  xpsrngd  20252  xpsringd  20410  rngqiprngim  21444  coe1mul2lem2  22429  scmatrngiso  22693  m2cpmrngiso  22915  cncfcnvcn  25084  isismt  28803  usgrf1oedg  29557  wlkiswwlks2lem5  30222  clwwlkvbij  30464  eupthres  30566  eupthp1  30567  f1oeq3dd  32974  cycpmconjvlem  33461  tocyccntz  33464  idomsubr  33630  dimkerim  34017  prodeq12sdv  36730  cbvsumdavw2  36807  cbvproddavw2  36808  poimirlem4  38275  poimirlem9  38280  rngoisoval  38628  frlmsnic  43308  sge0f1o  47096  nnfoctbdj  47170  3f1oss1  47812  f1oresf1o  48027  grimidvtxedg  48650  ushggricedg  48692  uhgrimisgrgric  48696  isubgr3stgrlem3  48733  uptrlem1  49988  uptrar  49994  uptr2  49999  oduoppcciso  50344