Theorem f1oeq3d 6713

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  –1-1-onto→wf1o 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440

This theorem is referenced by:  resdif  6737  f1osng  6757  f1oresrab  6999  fveqf1o  7175  isoini2  7210  oacomf1o  8396  mapsnf1o  8727  domss2  8923  dif1enlem  8943  wemapwe  9455  oef1o  9456  cnfcomlem  9457  cnfcom3  9462  cnfcom3clem  9463  infxpenc  9774  infxpenc2lem1  9775  infxpenc2  9778  ackbij2lem2  9996  hsmexlem1  10182  fsumss  15437  fsumcnv  15485  fprodss  15658  fprodcnv  15693  pwssnf1o  17209  catcisolem  17825  equivestrcsetc  17869  yoniso  18003  gsumpropd  18362  gsumpropd2lem  18363  xpsmnd  18425  xpsgrp  18694  gsumval3lem1  19506  gsumval3lem2  19507  gsumcom2  19576  coe1mul2lem2  21439  scmatrngiso  21685  m2cpmrngiso  21907  cncfcnvcn  24088  isismt  26895  usgrf1oedg  27574  wlkiswwlks2lem5  28238  clwwlkvbij  28477  eupthres  28579  eupthp1  28580  cycpmconjvlem  31408  tocyccntz  31411  dimkerim  31708  poimirlem4  35781  poimirlem9  35786  rngoisoval  36135  frlmsnic  40263  sge0f1o  43920  nnfoctbdj  43994  f1oresf1o  44782  ushrisomgr  45293