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 1536  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1osng  6889  f1o2sn  7161  fveqf1o  7321  oacomf1o  8601  marypha1lem  9470  oef1o  9735  cnfcomlem  9736  cnfcom2  9739  infxpenc  10055  pwfseqlem5  10700  pwfseq  10701  summolem3  15746  summo  15749  fsum  15752  prodmolem3  15965  prodmo  15968  fprod  15973  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumval3lem1  19937  gsumval3  19939  cncfcnvcn  24965  isismt  28556  f1ocnt  32809  erdsze2lem1  35187  ismtyval  37786  rngoisoval  37963  lautset  40064  pautsetN  40080  sticksstones3  42129  sticksstones20  42147  eldioph2lem1  42747  imasgim  43088  stoweidlem35  45990  stoweidlem39  45994  3f1oss1  47024  isubgr3stgrlem1  47868  isubgr3stgr  47877