Theorem f1oeq2d 6712

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 6705	. 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 1539  –1-1-onto→wf1o 6432

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440

This theorem is referenced by:  f1osng  6757  f1o2sn  7014  fveqf1o  7175  oacomf1o  8396  marypha1lem  9192  oef1o  9456  cnfcomlem  9457  cnfcom2  9460  infxpenc  9774  pwfseqlem5  10419  pwfseq  10420  summolem3  15426  summo  15429  fsum  15432  prodmolem3  15643  prodmo  15646  fprod  15651  gsumvalx  18360  gsumpropd  18362  gsumpropd2lem  18363  gsumval3lem1  19506  gsumval3  19508  cncfcnvcn  24088  isismt  26895  f1ocnt  31123  erdsze2lem1  33165  ismtyval  35958  rngoisoval  36135  lautset  38096  pautsetN  38112  sticksstones3  40104  sticksstones20  40122  eldioph2lem1  40582  imasgim  40925  stoweidlem35  43576  stoweidlem39  43580  isomgreqve  45277