Theorem f1oeq3d 6819

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  –1-1-onto→wf1o 6536

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is used by:  resdif  6844  f1osng  6865  f1oresrab  7126  fveqf1o  7308  isoini2  7345  oacomf1o  8566  mapsnf1o  8960  domss2  9148  dif1enlem  9168  infn0  9287  wemapwe  9691  oef1o  9692  cnfcomlem  9693  cnfcom3  9698  cnfcom3clem  9699  infxpenc  10090  infxpenc2lem1  10091  infxpenc2  10094  ackbij2lem2  10310  hsmexlem1  10497  fsumss  15884  fsumcnv  15932  fprodss  16108  fprodcnv  16143  pwssnf1o  17663  catcisolem  18278  equivestrcsetc  18319  yoniso  18452  gsumpropd  18860  gsumpropd2lem  18861  xpsmnd  18964  xpsgrp  19262  ghmqusker  19494  gsumval3lem1  20112  gsumval3lem2  20113  gsumcom2  20182  xpsrngd  20394  xpsringd  20555  rngqiprngim  21593  coe1mul2lem2  22580  scmatrngiso  22844  m2cpmrngiso  23069  cncfcnvcn  25239  isismt  28990  usgrf1oedg  29781  wlkiswwlks2lem5  30455  clwwlkvbij  30697  eupthres  30809  eupthp1  30810  f1oeq3dd  33216  cycpmconjvlem  33695  tocyccntz  33698  idomsubr  33864  dimkerim  34252  prodeq12sdv  36987  cbvsumdavw2  37064  cbvproddavw2  37065  poimirlem4  38522  poimirlem9  38527  rngoisoval  38891  frlmsnic  43584  sge0f1o  47361  nnfoctbdj  47435  3f1oss1  48114  f1oresf1o  48329  grimidvtxedg  48952  ushggricedg  48994  uhgrimisgrgric  48998  isubgr3stgrlem3  49035  uptrlem1  50287  uptrar  50293  uptr2  50298  oduoppcciso  50643