Theorem f1oeq3d 6827

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 6820	. 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 1541  –1-1-onto→wf1o 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is referenced by:  resdif  6851  f1osng  6871  f1oresrab  7121  fveqf1o  7297  isoini2  7332  oacomf1o  8561  mapsnf1o  8929  domss2  9132  dif1enlem  9152  dif1enlemOLD  9153  infn0  9303  wemapwe  9688  oef1o  9689  cnfcomlem  9690  cnfcom3  9695  cnfcom3clem  9696  infxpenc  10009  infxpenc2lem1  10010  infxpenc2  10013  ackbij2lem2  10231  hsmexlem1  10417  fsumss  15667  fsumcnv  15715  fprodss  15888  fprodcnv  15923  pwssnf1o  17440  catcisolem  18056  equivestrcsetc  18100  yoniso  18234  gsumpropd  18593  gsumpropd2lem  18594  xpsmnd  18661  xpsgrp  18938  gsumval3lem1  19767  gsumval3lem2  19768  gsumcom2  19837  xpsringd  20138  coe1mul2lem2  21781  scmatrngiso  22029  m2cpmrngiso  22251  cncfcnvcn  24432  isismt  27774  usgrf1oedg  28453  wlkiswwlks2lem5  29116  clwwlkvbij  29355  eupthres  29457  eupthp1  29458  cycpmconjvlem  32287  tocyccntz  32290  ghmqusker  32520  dimkerim  32700  poimirlem4  36480  poimirlem9  36485  rngoisoval  36833  frlmsnic  41107  sge0f1o  45084  nnfoctbdj  45158  f1oresf1o  45984  ushrisomgr  46495  xpsrngd  46666  rngqiprngim  46769