Theorem f1oeq2d 6768

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 6761	. 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 1541  –1-1-onto→wf1o 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1osng  6814  f1o2sn  7085  fveqf1o  7246  oacomf1o  8490  marypha1lem  9334  oef1o  9605  cnfcomlem  9606  cnfcom2  9609  infxpenc  9926  pwfseqlem5  10572  pwfseq  10573  summolem3  15635  summo  15638  fsum  15641  prodmolem3  15854  prodmo  15857  fprod  15862  gsumvalx  18599  gsumpropd  18601  gsumpropd2lem  18602  gsumval3lem1  19832  gsumval3  19834  cncfcnvcn  24873  isismt  28555  f1ocnt  32829  erdsze2lem1  35346  ismtyval  37940  rngoisoval  38117  lautset  40281  pautsetN  40297  sticksstones3  42341  sticksstones20  42359  eldioph2lem1  42944  imasgim  43284  stoweidlem35  46221  stoweidlem39  46225  3f1oss1  47263  isubgr3stgrlem1  48154  isubgr3stgr  48163