Theorem f1oeq2d 6816

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1osng  6863  f1o2sn  7138  fveqf1o  7300  oacomf1o  8546  marypha1lem  9389  oef1o  9663  cnfcomlem  9664  cnfcom2  9667  infxpenc  9998  pwfseqlem5  10643  pwfseq  10644  summolem3  15761  summo  15764  fsum  15767  prodmolem3  15983  prodmo  15986  fprod  15991  gsumvalx  18729  gsumpropd  18731  gsumpropd2lem  18732  gsumval3lem1  19970  gsumval3  19972  cncfcnvcn  25084  isismt  28803  f1ocnt  33145  erdsze2lem1  35695  ismtyval  38451  rngoisoval  38628  lautset  40856  pautsetN  40872  sticksstones3  42915  sticksstones20  42933  eldioph2lem1  43491  imasgim  43827  stoweidlem35  46749  stoweidlem39  46753  3f1oss1  47812  isubgr3stgrlem1  48731  isubgr3stgr  48740