Theorem f1oeq2d 6763

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 6756	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1osng  6809  f1o2sn  7084  fveqf1o  7246  oacomf1o  8490  marypha1lem  9336  oef1o  9610  cnfcomlem  9611  cnfcom2  9614  infxpenc  9931  pwfseqlem5  10577  pwfseq  10578  summolem3  15667  summo  15670  fsum  15673  prodmolem3  15889  prodmo  15892  fprod  15897  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumval3lem1  19871  gsumval3  19873  cncfcnvcn  24910  isismt  28620  f1ocnt  32892  erdsze2lem1  35431  ismtyval  38167  rngoisoval  38344  lautset  40574  pautsetN  40590  sticksstones3  42633  sticksstones20  42651  eldioph2lem1  43209  imasgim  43545  stoweidlem35  46478  stoweidlem39  46482  3f1oss1  47538  isubgr3stgrlem1  48457  isubgr3stgr  48466