Theorem f1oeq2d 6817

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  –1-1-onto→wf1o 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  f1osng  6864  f1o2sn  7139  fveqf1o  7301  oacomf1o  8549  marypha1lem  9392  oef1o  9666  cnfcomlem  9667  cnfcom2  9670  infxpenc  10001  pwfseqlem5  10647  pwfseq  10648  summolem3  15764  summo  15767  fsum  15770  prodmolem3  15986  prodmo  15989  fprod  15994  gsumvalx  18733  gsumpropd  18735  gsumpropd2lem  18736  gsumval3lem1  19974  gsumval3  19976  cncfcnvcn  25052  isismt  28768  f1ocnt  33085  erdsze2lem1  35593  ismtyval  38338  rngoisoval  38515  lautset  40745  pautsetN  40761  sticksstones3  42804  sticksstones20  42822  eldioph2lem1  43382  imasgim  43718  stoweidlem35  46640  stoweidlem39  46644  3f1oss1  47700  isubgr3stgrlem1  48619  isubgr3stgr  48628