Theorem f1oeq2d 6850

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-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐶))

Proof of Theorem f1oeq2d

Step	Hyp	Ref	Expression
1		f1oeq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq2 6843	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1osng  6898  f1o2sn  7177  fveqf1o  7341  oacomf1o  8611  marypha1lem  9462  oef1o  9736  cnfcomlem  9737  cnfcom2  9740  infxpenc  10136  pwfseqlem5  10787  pwfseq  10788  summolem3  15924  summo  15927  fsum  15930  prodmolem3  16144  prodmo  16147  fprod  16152  gsumvalx  18915  gsumpropd  18917  gsumpropd2lem  18918  imasgim  19534  gsumval3lem1  20170  gsumval3  20172  cncfcnvcn  25301  isismt  29054  f1ocnt  33488  erdsze2lem1  36176  ismtyval  39000  rngoisoval  39177  lautset  41405  pautsetN  41421  sticksstones3  43464  sticksstones20  43482  eldioph2lem1  44037  stoweidlem35  47318  stoweidlem39  47322  3f1oss1  48418  isubgr3stgrlem1  49337  isubgr3stgr  49346