Theorem f1oeq1d 6844

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 6837	. 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 1537  –1-1-onto→wf1o 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570

This theorem is referenced by:  f1orescnv  6864  f1osng  6890  f1ocoima  7323  f1ofvswap  7326  dif1en  9199  dif1enOLD  9201  cnfcomlem  9737  cnfcom2  9740  cnfcom3clem  9743  infxpenc  10056  infxpenc2lem2  10058  infxpenc2  10060  canthp1lem2  10691  pwfseqlem5  10701  pwfseq  10702  s2f1o  14952  s4f1o  14954  bitsf1ocnv  16478  yonffthlem  18339  grplactcnv  19074  eqgen  19212  znunithash  21601  tgpconncompeqg  24136  fcobijfs  32741  s2f1  32914  ccatws1f1o  32921  mgcf1o  32978  gsummpt2d  33035  gsumwrd2dccat  33053  indf1o  34005  subfacp1lem3  35167  subfacp1lem5  35169  ismrer1  37825  hvmap1o  41746  metakunt34  42220  3f1oss2  47026