Theorem f1oeq2d 6796

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  –1-1-onto→wf1o 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1osng  6841  f1o2sn  7114  fveqf1o  7277  oacomf1o  8529  marypha1lem  9384  oef1o  9651  cnfcomlem  9652  cnfcom2  9655  infxpenc  9971  pwfseqlem5  10616  pwfseq  10617  summolem3  15680  summo  15683  fsum  15686  prodmolem3  15899  prodmo  15902  fprod  15907  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumval3lem1  19835  gsumval3  19837  cncfcnvcn  24819  isismt  28461  f1ocnt  32725  erdsze2lem1  35190  ismtyval  37794  rngoisoval  37971  lautset  40076  pautsetN  40092  sticksstones3  42136  sticksstones20  42154  eldioph2lem1  42748  imasgim  43089  stoweidlem35  46033  stoweidlem39  46037  3f1oss1  47076  isubgr3stgrlem1  47965  isubgr3stgr  47974