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 1542  –1-1-onto→wf1o 6499

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1osng  6824  f1o2sn  7097  fveqf1o  7258  oacomf1o  8502  marypha1lem  9348  oef1o  9619  cnfcomlem  9620  cnfcom2  9623  infxpenc  9940  pwfseqlem5  10586  pwfseq  10587  summolem3  15649  summo  15652  fsum  15655  prodmolem3  15868  prodmo  15871  fprod  15876  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumval3lem1  19846  gsumval3  19848  cncfcnvcn  24887  isismt  28618  f1ocnt  32891  erdsze2lem1  35419  ismtyval  38051  rngoisoval  38228  lautset  40458  pautsetN  40474  sticksstones3  42518  sticksstones20  42536  eldioph2lem1  43117  imasgim  43457  stoweidlem35  46393  stoweidlem39  46397  3f1oss1  47435  isubgr3stgrlem1  48326  isubgr3stgr  48335