Theorem f1oeq2d 6611

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  –1-1-onto→wf1o 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362

This theorem is referenced by:  f1osng  6655  f1o2sn  6904  fveqf1o  7058  oacomf1o  8191  marypha1lem  8897  oef1o  9161  cnfcomlem  9162  cnfcom2  9165  infxpenc  9444  pwfseqlem5  10085  pwfseq  10086  summolem3  15071  summo  15074  fsum  15077  prodmolem3  15287  prodmo  15290  fprod  15295  gsumvalx  17886  gsumpropd  17888  gsumpropd2lem  17889  gsumval3lem1  19025  gsumval3  19027  cncfcnvcn  23529  isismt  26320  f1ocnt  30525  erdsze2lem1  32450  ismtyval  35093  rngoisoval  35270  lautset  37233  pautsetN  37249  eldioph2lem1  39377  imasgim  39720  stoweidlem35  42340  stoweidlem39  42344  isomgreqve  44010