Theorem f1oeq3d 6846

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 6839	. 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 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570

This theorem is referenced by:  resdif  6870  f1osng  6890  f1oresrab  7147  fveqf1o  7322  isoini2  7359  oacomf1o  8602  mapsnf1o  8978  domss2  9175  dif1enlem  9195  dif1enlemOLD  9196  infn0  9338  wemapwe  9735  oef1o  9736  cnfcomlem  9737  cnfcom3  9742  cnfcom3clem  9743  infxpenc  10056  infxpenc2lem1  10057  infxpenc2  10060  ackbij2lem2  10277  hsmexlem1  10464  fsumss  15758  fsumcnv  15806  fprodss  15981  fprodcnv  16016  pwssnf1o  17545  catcisolem  18164  equivestrcsetc  18208  yoniso  18342  gsumpropd  18704  gsumpropd2lem  18705  xpsmnd  18803  xpsgrp  19090  ghmqusker  19318  gsumval3lem1  19938  gsumval3lem2  19939  gsumcom2  20008  xpsrngd  20197  xpsringd  20346  rngqiprngim  21332  coe1mul2lem2  22287  scmatrngiso  22558  m2cpmrngiso  22780  cncfcnvcn  24966  isismt  28557  usgrf1oedg  29239  wlkiswwlks2lem5  29903  clwwlkvbij  30142  eupthres  30244  eupthp1  30245  cycpmconjvlem  33144  tocyccntz  33147  idomsubr  33291  dimkerim  33655  prodeq12sdv  36201  cbvsumdavw2  36278  cbvproddavw2  36279  poimirlem4  37611  poimirlem9  37616  rngoisoval  37964  frlmsnic  42527  sge0f1o  46338  nnfoctbdj  46412  3f1oss1  47025  f1oresf1o  47240  grimidvtxedg  47814  ushggricedg  47834  uhgrimisgrgric  47837  isubgr3stgrlem3  47871  oduoppcciso  48882