Theorem f1oeq1d 6819

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1orescnv  6840  f1osng  6867  f1ocoima  7307  f1ofvswap  7310  dif1en  9149  cnfcomlem  9671  cnfcom2  9674  cnfcom3clem  9677  infxpenc  10014  infxpenc2lem2  10016  infxpenc2  10018  canthp1lem2  10649  pwfseqlem5  10659  pwfseq  10660  s2f1o  14973  s4f1o  14975  bitsf1ocnv  16520  yonffthlem  18356  grplactcnv  19133  eqgen  19273  znunithash  21744  tgpconncompeqg  24300  fcobijfs  33112  fcobijfs2  33113  indf1o  33230  s2f1  33309  ccatws1f1o  33313  mgcf1o  33363  gsummpt2d  33409  gsumwrd2dccat  33438  subfacp1lem3  35687  subfacp1lem5  35689  ismrer1  38522  hvmap1o  42570  3f1oss2  47846  idfu1stf1o  49910  imaidfu  49921  fucoppc  50221  lmdran  50482