Theorem f1oeq2d 6826

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 6819	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  –1-1-onto→wf1o 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is referenced by:  f1osng  6871  f1o2sn  7136  fveqf1o  7297  oacomf1o  8561  marypha1lem  9424  oef1o  9689  cnfcomlem  9690  cnfcom2  9693  infxpenc  10009  pwfseqlem5  10654  pwfseq  10655  summolem3  15656  summo  15659  fsum  15662  prodmolem3  15873  prodmo  15876  fprod  15881  gsumvalx  18591  gsumpropd  18593  gsumpropd2lem  18594  gsumval3lem1  19767  gsumval3  19769  cncfcnvcn  24432  isismt  27774  f1ocnt  32000  erdsze2lem1  34182  ismtyval  36656  rngoisoval  36833  lautset  38941  pautsetN  38957  sticksstones3  40952  sticksstones20  40970  eldioph2lem1  41483  imasgim  41827  stoweidlem35  44737  stoweidlem39  44741  isomgreqve  46479