Theorem f1oeq3d 6841

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 6834	. 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 1533  –1-1-onto→wf1o 6552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560

This theorem is referenced by:  resdif  6865  f1osng  6885  f1oresrab  7142  fveqf1o  7318  isoini2  7353  oacomf1o  8592  mapsnf1o  8964  domss2  9167  dif1enlem  9187  dif1enlemOLD  9188  infn0  9338  wemapwe  9728  oef1o  9729  cnfcomlem  9730  cnfcom3  9735  cnfcom3clem  9736  infxpenc  10049  infxpenc2lem1  10050  infxpenc2  10053  ackbij2lem2  10271  hsmexlem1  10457  fsumss  15711  fsumcnv  15759  fprodss  15932  fprodcnv  15967  pwssnf1o  17487  catcisolem  18106  equivestrcsetc  18150  yoniso  18284  gsumpropd  18645  gsumpropd2lem  18646  xpsmnd  18741  xpsgrp  19022  ghmqusker  19245  gsumval3lem1  19867  gsumval3lem2  19868  gsumcom2  19937  xpsrngd  20126  xpsringd  20275  rngqiprngim  21201  coe1mul2lem2  22194  scmatrngiso  22458  m2cpmrngiso  22680  cncfcnvcn  24866  isismt  28358  usgrf1oedg  29040  wlkiswwlks2lem5  29704  clwwlkvbij  29943  eupthres  30045  eupthp1  30046  cycpmconjvlem  32883  tocyccntz  32886  idomsubr  33020  dimkerim  33358  poimirlem4  37130  poimirlem9  37135  rngoisoval  37483  frlmsnic  41801  sge0f1o  45799  nnfoctbdj  45873  f1oresf1o  46699  grimidvtxedg  47252  ushggricedg  47271