Theorem f1oeq3d 6777

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 6770	. 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 1542  –1-1-onto→wf1o 6497

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  resdif  6801  f1osng  6822  f1oresrab  7080  fveqf1o  7257  isoini2  7294  oacomf1o  8500  mapsnf1o  8887  domss2  9074  dif1enlem  9094  infn0  9212  wemapwe  9618  oef1o  9619  cnfcomlem  9620  cnfcom3  9625  cnfcom3clem  9626  infxpenc  9940  infxpenc2lem1  9941  infxpenc2  9944  ackbij2lem2  10161  hsmexlem1  10348  fsumss  15687  fsumcnv  15735  fprodss  15913  fprodcnv  15948  pwssnf1o  17462  catcisolem  18077  equivestrcsetc  18118  yoniso  18251  gsumpropd  18646  gsumpropd2lem  18647  xpsmnd  18745  xpsgrp  19035  ghmqusker  19262  gsumval3lem1  19880  gsumval3lem2  19881  gsumcom2  19950  xpsrngd  20160  xpsringd  20312  rngqiprngim  21302  coe1mul2lem2  22233  scmatrngiso  22501  m2cpmrngiso  22723  cncfcnvcn  24892  isismt  28602  usgrf1oedg  29276  wlkiswwlks2lem5  29941  clwwlkvbij  30183  eupthres  30285  eupthp1  30286  f1oeq3dd  32702  cycpmconjvlem  33202  tocyccntz  33205  idomsubr  33370  dimkerim  33771  prodeq12sdv  36400  cbvsumdavw2  36477  cbvproddavw2  36478  poimirlem4  37945  poimirlem9  37950  rngoisoval  38298  frlmsnic  42985  sge0f1o  46810  nnfoctbdj  46884  3f1oss1  47523  f1oresf1o  47738  grimidvtxedg  48361  ushggricedg  48403  uhgrimisgrgric  48407  isubgr3stgrlem3  48444  uptrlem1  49685  uptrar  49691  uptr2  49696  oduoppcciso  50041