Theorem f1oeq2d 6818

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 6811	. 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 6536

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is used by:  f1osng  6865  f1o2sn  7143  fveqf1o  7308  oacomf1o  8566  marypha1lem  9418  oef1o  9692  cnfcomlem  9693  cnfcom2  9696  infxpenc  10090  pwfseqlem5  10741  pwfseq  10742  summolem3  15873  summo  15876  fsum  15879  prodmolem3  16093  prodmo  16096  fprod  16101  gsumvalx  18858  gsumpropd  18860  gsumpropd2lem  18861  gsumval3lem1  20112  gsumval3  20114  cncfcnvcn  25239  isismt  28990  f1ocnt  33385  erdsze2lem1  35947  ismtyval  38714  rngoisoval  38891  lautset  41119  pautsetN  41135  sticksstones3  43178  sticksstones20  43196  eldioph2lem1  43750  imasgim  44086  stoweidlem35  47014  stoweidlem39  47018  3f1oss1  48114  isubgr3stgrlem1  49033  isubgr3stgr  49042