Theorem f1oeq2d 6378

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1656  –1-1-onto→wf1o 6126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134

This theorem is referenced by:  f1osng  6422  f1o2sn  6663  fveqf1o  6817  oacomf1o  7917  marypha1lem  8614  oef1o  8879  cnfcomlem  8880  cnfcom2  8883  infxpenc  9161  pwfseqlem5  9807  pwfseq  9808  summolem3  14829  summo  14832  fsum  14835  prodmolem3  15043  prodmo  15046  fprod  15051  gsumvalx  17630  gsumpropd  17632  gsumpropd2lem  17633  gsumval3lem1  18666  gsumval3  18668  cncfcnvcn  23101  isismt  25853  f1ocnt  30102  erdsze2lem1  31727  ismtyval  34136  rngoisoval  34313  lautset  36152  pautsetN  36168  eldioph2lem1  38162  imasgim  38508  stoweidlem35  41040  stoweidlem39  41044  isomgreqve  42557