Theorem f1oeq2d 6586

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  –1-1-onto→wf1o 6323

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  f1osng  6630  f1o2sn  6881  fveqf1o  7037  oacomf1o  8174  marypha1lem  8881  oef1o  9145  cnfcomlem  9146  cnfcom2  9149  infxpenc  9429  pwfseqlem5  10074  pwfseq  10075  summolem3  15063  summo  15066  fsum  15069  prodmolem3  15279  prodmo  15282  fprod  15287  gsumvalx  17878  gsumpropd  17880  gsumpropd2lem  17881  gsumval3lem1  19018  gsumval3  19020  cncfcnvcn  23530  isismt  26328  f1ocnt  30551  erdsze2lem1  32563  ismtyval  35238  rngoisoval  35415  lautset  37378  pautsetN  37394  eldioph2lem1  39701  imasgim  40044  stoweidlem35  42677  stoweidlem39  42681  isomgreqve  44343