Theorem f1oeq2d 6825

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  f1osng  6872  f1o2sn  7150  fveqf1o  7314  oacomf1o  8580  marypha1lem  9432  oef1o  9706  cnfcomlem  9707  cnfcom2  9710  infxpenc  10104  pwfseqlem5  10755  pwfseq  10756  summolem3  15889  summo  15892  fsum  15895  prodmolem3  16109  prodmo  16112  fprod  16117  gsumvalx  18874  gsumpropd  18876  gsumpropd2lem  18877  gsumval3lem1  20128  gsumval3  20130  cncfcnvcn  25255  isismt  29006  f1ocnt  33442  erdsze2lem1  36058  ismtyval  38843  rngoisoval  39020  lautset  41248  pautsetN  41264  sticksstones3  43307  sticksstones20  43325  eldioph2lem1  43880  imasgim  44211  stoweidlem35  47153  stoweidlem39  47157  3f1oss1  48253  isubgr3stgrlem1  49172  isubgr3stgr  49181