Theorem f1oeq2d 6696

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 6689	. 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 1539  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1osng  6740  f1o2sn  6996  fveqf1o  7155  oacomf1o  8358  marypha1lem  9122  oef1o  9386  cnfcomlem  9387  cnfcom2  9390  infxpenc  9705  pwfseqlem5  10350  pwfseq  10351  summolem3  15354  summo  15357  fsum  15360  prodmolem3  15571  prodmo  15574  fprod  15579  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumval3lem1  19421  gsumval3  19423  cncfcnvcn  23994  isismt  26799  f1ocnt  31025  erdsze2lem1  33065  ismtyval  35885  rngoisoval  36062  lautset  38023  pautsetN  38039  sticksstones3  40032  sticksstones20  40050  eldioph2lem1  40498  imasgim  40841  stoweidlem35  43466  stoweidlem39  43470  isomgreqve  45165