Theorem f1oeq2d 6776

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 6769	. 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 1542  –1-1-onto→wf1o 6497

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1osng  6822  f1o2sn  7095  fveqf1o  7257  oacomf1o  8500  marypha1lem  9346  oef1o  9619  cnfcomlem  9620  cnfcom2  9623  infxpenc  9940  pwfseqlem5  10586  pwfseq  10587  summolem3  15676  summo  15679  fsum  15682  prodmolem3  15898  prodmo  15901  fprod  15906  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumval3lem1  19880  gsumval3  19882  cncfcnvcn  24892  isismt  28602  f1ocnt  32873  erdsze2lem1  35385  ismtyval  38121  rngoisoval  38298  lautset  40528  pautsetN  40544  sticksstones3  42587  sticksstones20  42605  eldioph2lem1  43192  imasgim  43528  stoweidlem35  46463  stoweidlem39  46467  3f1oss1  47523  isubgr3stgrlem1  48442  isubgr3stgr  48451