Theorem f1oeq3d 6851

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-1onto𝐴 ↔ 𝐹:𝐶⟶1-1onto𝐵))

Proof of Theorem f1oeq3d

Step	Hyp	Ref	Expression
1		f1oeq3d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq3 6844	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶1-1onto𝐴 ↔ 𝐹:𝐶⟶1-1onto𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐹:𝐶⟶1-1onto𝐴 ↔ 𝐹:𝐶⟶1-1onto𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  resdif  6876  f1osng  6898  f1oresrab  7160  fveqf1o  7341  isoini2  7378  oacomf1o  8611  mapsnf1o  9005  domss2  9193  dif1enlem  9213  infn0  9332  wemapwe  9735  oef1o  9736  cnfcomlem  9737  cnfcom3  9742  cnfcom3clem  9743  infxpenc  10136  infxpenc2lem1  10137  infxpenc2  10140  ackbij2lem2  10356  hsmexlem1  10543  fsumss  15935  fsumcnv  15983  fprodss  16159  fprodcnv  16194  pwssnf1o  17720  catcisolem  18335  equivestrcsetc  18376  yoniso  18509  gsumpropd  18917  gsumpropd2lem  18918  xpsmnd  19021  xpsgrp  19319  ghmqusker  19552  gsumval3lem1  20170  gsumval3lem2  20171  gsumcom2  20240  xpsrngd  20452  xpsringd  20613  rngqiprngim  21651  coe1mul2lem2  22642  scmatrngiso  22906  m2cpmrngiso  23131  cncfcnvcn  25301  isismt  29054  usgrf1oedg  29845  wlkiswwlks2lem5  30519  clwwlkvbij  30761  eupthres  30873  eupthp1  30874  f1oeq3dd  33321  cycpmconjvlem  33801  tocyccntz  33804  idomsubr  33975  dimkerim  34370  prodeq12sdv  37222  cbvsumdavw2  37299  cbvproddavw2  37300  poimirlem4  38810  poimirlem9  38815  rngoisoval  39177  frlmsnic  43870  sge0f1o  47665  nnfoctbdj  47739  3f1oss1  48418  f1oresf1o  48633  grimidvtxedg  49256  ushggricedg  49298  uhgrimisgrgric  49302  isubgr3stgrlem3  49339  uptrlem1  50657  uptrar  50663  uptr2  50668  oduoppcciso  51035