Theorem f1oeq2d 6771

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 6764	. 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 6492

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 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  f1osng  6817  f1o2sn  7090  fveqf1o  7251  oacomf1o  8494  marypha1lem  9340  oef1o  9613  cnfcomlem  9614  cnfcom2  9617  infxpenc  9934  pwfseqlem5  10580  pwfseq  10581  summolem3  15670  summo  15673  fsum  15676  prodmolem3  15892  prodmo  15895  fprod  15900  gsumvalx  18638  gsumpropd  18640  gsumpropd2lem  18641  gsumval3lem1  19874  gsumval3  19876  cncfcnvcn  24905  isismt  28619  f1ocnt  32891  erdsze2lem1  35404  ismtyval  38138  rngoisoval  38315  lautset  40545  pautsetN  40561  sticksstones3  42604  sticksstones20  42622  eldioph2lem1  43209  imasgim  43549  stoweidlem35  46484  stoweidlem39  46488  3f1oss1  47538  isubgr3stgrlem1  48457  isubgr3stgr  48466