Theorem f1oeq2d 6858

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 6851	. 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 1537  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  f1osng  6903  f1o2sn  7176  fveqf1o  7338  oacomf1o  8621  marypha1lem  9502  oef1o  9767  cnfcomlem  9768  cnfcom2  9771  infxpenc  10087  pwfseqlem5  10732  pwfseq  10733  summolem3  15762  summo  15765  fsum  15768  prodmolem3  15981  prodmo  15984  fprod  15989  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumval3lem1  19947  gsumval3  19949  cncfcnvcn  24971  isismt  28560  f1ocnt  32807  erdsze2lem1  35171  ismtyval  37760  rngoisoval  37937  lautset  40039  pautsetN  40055  sticksstones3  42105  sticksstones20  42123  eldioph2lem1  42716  imasgim  43057  stoweidlem35  45956  stoweidlem39  45960  3f1oss1  46990