Theorem f1oeq2d 6613

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 6607	. 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 6356

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  f1osng  6657  f1o2sn  6906  fveqf1o  7060  oacomf1o  8193  marypha1lem  8899  oef1o  9163  cnfcomlem  9164  cnfcom2  9167  infxpenc  9446  pwfseqlem5  10087  pwfseq  10088  summolem3  15073  summo  15076  fsum  15079  prodmolem3  15289  prodmo  15292  fprod  15297  gsumvalx  17888  gsumpropd  17890  gsumpropd2lem  17891  gsumval3lem1  19027  gsumval3  19029  cncfcnvcn  23531  isismt  26322  f1ocnt  30527  erdsze2lem1  32452  ismtyval  35080  rngoisoval  35257  lautset  37220  pautsetN  37236  eldioph2lem1  39364  imasgim  39707  stoweidlem35  42327  stoweidlem39  42331  isomgreqve  43997