Theorem f1oeq2d 6813

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 6806	. 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 6532

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1osng  6860  f1o2sn  7138  fveqf1o  7303  oacomf1o  8552  marypha1lem  9403  oef1o  9677  cnfcomlem  9678  cnfcom2  9681  infxpenc  10021  pwfseqlem5  10672  pwfseq  10673  summolem3  15800  summo  15803  fsum  15806  prodmolem3  16020  prodmo  16023  fprod  16028  gsumvalx  18778  gsumpropd  18780  gsumpropd2lem  18781  gsumval3lem1  20032  gsumval3  20034  cncfcnvcn  25153  isismt  28876  f1ocnt  33271  erdsze2lem1  35782  ismtyval  38550  rngoisoval  38727  lautset  40955  pautsetN  40971  sticksstones3  43014  sticksstones20  43032  eldioph2lem1  43605  imasgim  43941  stoweidlem35  46863  stoweidlem39  46867  3f1oss1  47963  isubgr3stgrlem1  48882  isubgr3stgr  48891