Theorem f1oeq2d 6844

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
f1oeq2d	⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Proof of Theorem f1oeq2d

Step	Hyp	Ref	Expression
1		f1oeq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq2 6837	. 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 1540  –1-1-onto→wf1o 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1osng  6889  f1o2sn  7162  fveqf1o  7322  oacomf1o  8603  marypha1lem  9473  oef1o  9738  cnfcomlem  9739  cnfcom2  9742  infxpenc  10058  pwfseqlem5  10703  pwfseq  10704  summolem3  15750  summo  15753  fsum  15756  prodmolem3  15969  prodmo  15972  fprod  15977  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumval3lem1  19923  gsumval3  19925  cncfcnvcn  24952  isismt  28542  f1ocnt  32804  erdsze2lem1  35208  ismtyval  37807  rngoisoval  37984  lautset  40084  pautsetN  40100  sticksstones3  42149  sticksstones20  42167  eldioph2lem1  42771  imasgim  43112  stoweidlem35  46050  stoweidlem39  46054  3f1oss1  47087  isubgr3stgrlem1  47933  isubgr3stgr  47942