Theorem f1oeq2d 6760

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 6753	. 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 6481

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 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1osng  6805  f1o2sn  7076  fveqf1o  7239  oacomf1o  8483  marypha1lem  9323  oef1o  9594  cnfcomlem  9595  cnfcom2  9598  infxpenc  9912  pwfseqlem5  10557  pwfseq  10558  summolem3  15621  summo  15624  fsum  15627  prodmolem3  15840  prodmo  15843  fprod  15848  gsumvalx  18550  gsumpropd  18552  gsumpropd2lem  18553  gsumval3lem1  19784  gsumval3  19786  cncfcnvcn  24817  isismt  28479  f1ocnt  32745  erdsze2lem1  35176  ismtyval  37780  rngoisoval  37957  lautset  40061  pautsetN  40077  sticksstones3  42121  sticksstones20  42139  eldioph2lem1  42733  imasgim  43073  stoweidlem35  46016  stoweidlem39  46020  3f1oss1  47059  isubgr3stgrlem1  47950  isubgr3stgr  47959