Theorem f1oeq2d 6814

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 6807	. 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 1540  –1-1-onto→wf1o 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is referenced by:  f1osng  6859  f1o2sn  7132  fveqf1o  7295  oacomf1o  8577  marypha1lem  9445  oef1o  9712  cnfcomlem  9713  cnfcom2  9716  infxpenc  10032  pwfseqlem5  10677  pwfseq  10678  summolem3  15730  summo  15733  fsum  15736  prodmolem3  15949  prodmo  15952  fprod  15957  gsumvalx  18654  gsumpropd  18656  gsumpropd2lem  18657  gsumval3lem1  19886  gsumval3  19888  cncfcnvcn  24870  isismt  28513  f1ocnt  32779  erdsze2lem1  35225  ismtyval  37824  rngoisoval  38001  lautset  40101  pautsetN  40117  sticksstones3  42161  sticksstones20  42179  eldioph2lem1  42783  imasgim  43124  stoweidlem35  46064  stoweidlem39  46068  3f1oss1  47104  isubgr3stgrlem1  47978  isubgr3stgr  47987