Theorem f1oeq2d 6802

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  f1osng  6849  f1o2sn  7124  fveqf1o  7286  oacomf1o  8534  marypha1lem  9379  oef1o  9653  cnfcomlem  9654  cnfcom2  9657  infxpenc  9974  pwfseqlem5  10621  pwfseq  10622  summolem3  15741  summo  15744  fsum  15747  prodmolem3  15963  prodmo  15966  fprod  15971  gsumvalx  18710  gsumpropd  18712  gsumpropd2lem  18713  gsumval3lem1  19945  gsumval3  19947  cncfcnvcn  24984  isismt  28700  f1ocnt  32999  erdsze2lem1  35550  ismtyval  38296  rngoisoval  38473  lautset  40703  pautsetN  40719  sticksstones3  42762  sticksstones20  42780  eldioph2lem1  43338  imasgim  43674  stoweidlem35  46606  stoweidlem39  46610  3f1oss1  47666  isubgr3stgrlem1  48585  isubgr3stgr  48594