Theorem f1oeq123d 6752

Description: Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)

Hypotheses

Ref	Expression
f1eq123d.1	⊢ (𝜑 → 𝐹 = 𝐺)
f1eq123d.2	⊢ (𝜑 → 𝐴 = 𝐵)
f1eq123d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
f1oeq123d	⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Proof of Theorem f1oeq123d

Step	Hyp	Ref	Expression
1		f1eq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1oeq1 6746	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1oeq2 6747	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
6	4, 5	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1oeq3 6748	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 305	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  –1-1-onto→wf1o 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483

This theorem is referenced by:  f1oprswap  6802  f1oprg  6803  f1ossf1o  7056  cnfcom  9585  ackbij2lem2  10125  idffth  17837  ressffth  17842  symgval  19278  symg1bas  19298  symg2bas  19300  symgfixels  19341  symgfixelsi  19342  rnghmf1o  20365  rhmf1o  20403  mat1f1o  22388  ushgredgedg  29202  ushgredgedgloop  29204  trlreslem  29671  wlknwwlksnbij  29861  wwlksnextbij  29875  clwlknf1oclwwlkn  30056  eupth0  30186  eupthp1  30188  foresf1o  32476  f1ocnt  32774  indf1ofs  32839  gsumwrd2dccat  33039  symgcom  33044  cycpmcl  33077  cycpmconjslem2  33116  nsgqusf1o  33373  1arithidomlem2  33493  1arithidom  33494  dimkerim  33632  eulerpartgbij  34377  eulerpartlemn  34386  reprpmtf1o  34631  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem28  37688  wessf1ornlem  45222  disjf1o  45228  ssnnf1octb  45231  sge0fodjrnlem  46454  f1oresf1orab  47320  isgrim  47913  isubgrgrim  47960  isgrlim  48013  uspgrlim  48023  grlimedgclnbgr  48026  grlimgrtri  48034  grilcbri2  48042  gpg5grlim  48124  swapf1f1o  49307  swapf2f1o  49308  swapf2f1oa  49309  swapf2f1oaALT  49310  fucoppc  49442