Theorem f1oeq2d 6770

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 6763	. 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 6491

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1osng  6816  f1o2sn  7087  fveqf1o  7248  oacomf1o  8492  marypha1lem  9336  oef1o  9607  cnfcomlem  9608  cnfcom2  9611  infxpenc  9928  pwfseqlem5  10574  pwfseq  10575  summolem3  15637  summo  15640  fsum  15643  prodmolem3  15856  prodmo  15859  fprod  15864  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumval3lem1  19834  gsumval3  19836  cncfcnvcn  24875  isismt  28606  f1ocnt  32880  erdsze2lem1  35397  ismtyval  38001  rngoisoval  38178  lautset  40342  pautsetN  40358  sticksstones3  42402  sticksstones20  42420  eldioph2lem1  43002  imasgim  43342  stoweidlem35  46279  stoweidlem39  46283  3f1oss1  47321  isubgr3stgrlem1  48212  isubgr3stgr  48221