Theorem f1oeq1d 6812

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 6805	. 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 6532

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1orescnv  6833  f1osng  6860  f1ocoima  7304  f1ofvswap  7307  dif1en  9156  cnfcomlem  9678  cnfcom2  9681  cnfcom3clem  9684  infxpenc  10021  infxpenc2lem2  10023  infxpenc2  10025  canthp1lem2  10662  pwfseqlem5  10672  pwfseq  10673  s2f1o  14987  s4f1o  14989  bitsf1ocnv  16534  yonffthlem  18370  grplactcnv  19166  eqgen  19306  znunithash  21777  tgpconncompeqg  24338  fcobijfs  33192  fcobijfs2  33193  indf1o  33310  s2f1  33389  ccatws1f1o  33393  mgcf1o  33443  gsummpt2d  33489  gsumwrd2dccat  33518  subfacp1lem3  35761  subfacp1lem5  35763  ismrer1  38588  hvmap1o  42636  3f1oss2  47964  idfu1stf1o  50025  imaidfu  50036  fucoppc  50336  lmdran  50597