Theorem f1oeq2d 6778

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 6771	. 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 1540  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1osng  6823  f1o2sn  7096  fveqf1o  7259  oacomf1o  8506  marypha1lem  9360  oef1o  9627  cnfcomlem  9628  cnfcom2  9631  infxpenc  9947  pwfseqlem5  10592  pwfseq  10593  summolem3  15656  summo  15659  fsum  15662  prodmolem3  15875  prodmo  15878  fprod  15883  gsumvalx  18579  gsumpropd  18581  gsumpropd2lem  18582  gsumval3lem1  19811  gsumval3  19813  cncfcnvcn  24795  isismt  28437  f1ocnt  32698  erdsze2lem1  35163  ismtyval  37767  rngoisoval  37944  lautset  40049  pautsetN  40065  sticksstones3  42109  sticksstones20  42127  eldioph2lem1  42721  imasgim  43062  stoweidlem35  46006  stoweidlem39  46010  3f1oss1  47049  isubgr3stgrlem1  47938  isubgr3stgr  47947