Theorem f1oeq2d 6830

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  –1-1-onto→wf1o 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1osng  6875  f1o2sn  7140  fveqf1o  7301  oacomf1o  8565  marypha1lem  9428  oef1o  9693  cnfcomlem  9694  cnfcom2  9697  infxpenc  10013  pwfseqlem5  10658  pwfseq  10659  summolem3  15660  summo  15663  fsum  15666  prodmolem3  15877  prodmo  15880  fprod  15885  gsumvalx  18595  gsumpropd  18597  gsumpropd2lem  18598  gsumval3lem1  19773  gsumval3  19775  cncfcnvcn  24441  isismt  27785  f1ocnt  32013  erdsze2lem1  34194  ismtyval  36668  rngoisoval  36845  lautset  38953  pautsetN  38969  sticksstones3  40964  sticksstones20  40982  eldioph2lem1  41498  imasgim  41842  stoweidlem35  44751  stoweidlem39  44755  isomgreqve  46493