Theorem f1oeq2d 6820

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 6813	. 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 1570  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1osng  6867  f1o2sn  7144  fveqf1o  7309  oacomf1o  8556  marypha1lem  9400  oef1o  9674  cnfcomlem  9675  cnfcom2  9678  infxpenc  10018  pwfseqlem5  10663  pwfseq  10664  summolem3  15788  summo  15791  fsum  15794  prodmolem3  16010  prodmo  16013  fprod  16018  gsumvalx  18766  gsumpropd  18768  gsumpropd2lem  18769  gsumval3lem1  20019  gsumval3  20021  cncfcnvcn  25135  isismt  28854  f1ocnt  33215  erdsze2lem1  35732  ismtyval  38509  rngoisoval  38686  lautset  40914  pautsetN  40930  sticksstones3  42973  sticksstones20  42991  eldioph2lem1  43549  imasgim  43885  stoweidlem35  46807  stoweidlem39  46811  3f1oss1  47870  isubgr3stgrlem1  48789  isubgr3stgr  48798