Theorem f1oeq2d 6829

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 6822	. 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 1541  –1-1-onto→wf1o 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is referenced by:  f1osng  6874  f1o2sn  7142  fveqf1o  7303  oacomf1o  8567  marypha1lem  9430  oef1o  9695  cnfcomlem  9696  cnfcom2  9699  infxpenc  10015  pwfseqlem5  10660  pwfseq  10661  summolem3  15664  summo  15667  fsum  15670  prodmolem3  15881  prodmo  15884  fprod  15889  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumval3lem1  19814  gsumval3  19816  cncfcnvcn  24665  isismt  28040  f1ocnt  32268  erdsze2lem1  34480  ismtyval  36971  rngoisoval  37148  lautset  39256  pautsetN  39272  sticksstones3  41270  sticksstones20  41288  eldioph2lem1  41800  imasgim  42144  stoweidlem35  45050  stoweidlem39  45054  isomgreqve  46792