Theorem f1oeq1d 6763

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 6756	. 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 6485

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1orescnv  6783  f1osng  6809  f1ocoima  7244  f1ofvswap  7247  dif1en  9084  dif1enOLD  9086  cnfcomlem  9614  cnfcom2  9617  cnfcom3clem  9620  infxpenc  9931  infxpenc2lem2  9933  infxpenc2  9935  canthp1lem2  10566  pwfseqlem5  10576  pwfseq  10577  s2f1o  14842  s4f1o  14844  bitsf1ocnv  16374  yonffthlem  18207  grplactcnv  18941  eqgen  19079  znunithash  21490  tgpconncompeqg  24016  fcobijfs  32684  fcobijfs2  32685  indf1o  32826  s2f1  32905  ccatws1f1o  32912  mgcf1o  32964  gsummpt2d  33021  gsumwrd2dccat  33039  subfacp1lem3  35174  subfacp1lem5  35176  ismrer1  37837  hvmap1o  41762  3f1oss2  47080  idfu1stf1o  49104  imaidfu  49115  fucoppc  49415  lmdran  49676