Theorem f1oeq2d 6799

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 6792	. 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 6513

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1osng  6844  f1o2sn  7117  fveqf1o  7280  oacomf1o  8532  marypha1lem  9391  oef1o  9658  cnfcomlem  9659  cnfcom2  9662  infxpenc  9978  pwfseqlem5  10623  pwfseq  10624  summolem3  15687  summo  15690  fsum  15693  prodmolem3  15906  prodmo  15909  fprod  15914  gsumvalx  18610  gsumpropd  18612  gsumpropd2lem  18613  gsumval3lem1  19842  gsumval3  19844  cncfcnvcn  24826  isismt  28468  f1ocnt  32732  erdsze2lem1  35197  ismtyval  37801  rngoisoval  37978  lautset  40083  pautsetN  40099  sticksstones3  42143  sticksstones20  42161  eldioph2lem1  42755  imasgim  43096  stoweidlem35  46040  stoweidlem39  46044  3f1oss1  47080  isubgr3stgrlem1  47969  isubgr3stgr  47978