Theorem f1oeq1d 6813

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
f1oeq1d	⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Proof of Theorem f1oeq1d

Step	Hyp	Ref	Expression
1		f1oeq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1oeq1 6806	. 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 6530

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is referenced by:  f1orescnv  6833  f1osng  6859  f1ocoima  7296  f1ofvswap  7299  dif1en  9174  dif1enOLD  9176  cnfcomlem  9713  cnfcom2  9716  cnfcom3clem  9719  infxpenc  10032  infxpenc2lem2  10034  infxpenc2  10036  canthp1lem2  10667  pwfseqlem5  10677  pwfseq  10678  s2f1o  14935  s4f1o  14937  bitsf1ocnv  16463  yonffthlem  18294  grplactcnv  19026  eqgen  19164  znunithash  21525  tgpconncompeqg  24050  fcobijfs  32700  indf1o  32841  s2f1  32920  ccatws1f1o  32927  mgcf1o  32983  gsummpt2d  33043  gsumwrd2dccat  33061  subfacp1lem3  35204  subfacp1lem5  35206  ismrer1  37862  hvmap1o  41782  metakunt34  42251  3f1oss2  47105  imaidfu  49069