Theorem f1oeq2d 6819

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 6812	. 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 1533  –1-1-onto→wf1o 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is referenced by:  f1osng  6864  f1o2sn  7132  fveqf1o  7293  oacomf1o  8560  marypha1lem  9423  oef1o  9688  cnfcomlem  9689  cnfcom2  9692  infxpenc  10008  pwfseqlem5  10653  pwfseq  10654  summolem3  15656  summo  15659  fsum  15662  prodmolem3  15873  prodmo  15876  fprod  15881  gsumvalx  18598  gsumpropd  18600  gsumpropd2lem  18601  gsumval3lem1  19814  gsumval3  19816  cncfcnvcn  24767  isismt  28220  f1ocnt  32448  erdsze2lem1  34649  ismtyval  37124  rngoisoval  37301  lautset  39409  pautsetN  39425  sticksstones3  41423  sticksstones20  41441  eldioph2lem1  41953  imasgim  42297  stoweidlem35  45202  stoweidlem39  45206  isomgreqve  46944