Theorem f1oeq2d 6759

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 6752	. 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 6480

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1osng  6804  f1o2sn  7075  fveqf1o  7236  oacomf1o  8480  marypha1lem  9317  oef1o  9588  cnfcomlem  9589  cnfcom2  9592  infxpenc  9909  pwfseqlem5  10554  pwfseq  10555  summolem3  15621  summo  15624  fsum  15627  prodmolem3  15840  prodmo  15843  fprod  15848  gsumvalx  18584  gsumpropd  18586  gsumpropd2lem  18587  gsumval3lem1  19817  gsumval3  19819  cncfcnvcn  24846  isismt  28512  f1ocnt  32782  erdsze2lem1  35247  ismtyval  37848  rngoisoval  38025  lautset  40129  pautsetN  40145  sticksstones3  42189  sticksstones20  42207  eldioph2lem1  42801  imasgim  43141  stoweidlem35  46081  stoweidlem39  46085  3f1oss1  47114  isubgr3stgrlem1  48005  isubgr3stgr  48014