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 18	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  –1-1-onto→wf1o 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541

This theorem is referenced by:  f1orescnv  6834  f1osng  6861  f1ocoima  7299  f1ofvswap  7302  dif1en  9142  cnfcomlem  9664  cnfcom2  9667  cnfcom3clem  9670  infxpenc  9998  infxpenc2lem2  10000  infxpenc2  10002  canthp1lem2  10634  pwfseqlem5  10644  pwfseq  10645  s2f1o  14949  s4f1o  14951  bitsf1ocnv  16498  yonffthlem  18334  grplactcnv  19105  eqgen  19245  znunithash  21679  tgpconncompeqg  24234  fcobijfs  33003  fcobijfs2  33004  indf1o  33121  s2f1  33202  ccatws1f1o  33208  mgcf1o  33260  gsummpt2d  33306  gsumwrd2dccat  33335  subfacp1lem3  35569  subfacp1lem5  35571  ismrer1  38372  hvmap1o  42422  3f1oss2  47697  idfu1stf1o  49757  imaidfu  49768  fucoppc  50068  lmdran  50329