Theorem f1oeq123d 6765

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 6759	. . 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 6760	. . 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 6761	. . 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 6488

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496

This theorem is referenced by:  f1oprswap  6816  f1oprg  6817  f1ossf1o  7070  cnfcom  9601  ackbij2lem2  10141  idffth  17850  ressffth  17855  symgval  19291  symg1bas  19311  symg2bas  19313  symgfixels  19354  symgfixelsi  19355  rnghmf1o  20379  rhmf1o  20417  mat1f1o  22413  ushgredgedg  29228  ushgredgedgloop  29230  trlreslem  29697  wlknwwlksnbij  29887  wwlksnextbij  29901  clwlknf1oclwwlkn  30085  eupth0  30215  eupthp1  30217  foresf1o  32505  f1ocnt  32808  indf1ofs  32876  gsumwrd2dccat  33088  symgcom  33093  cycpmcl  33126  cycpmconjslem2  33165  nsgqusf1o  33425  1arithidomlem2  33545  1arithidom  33546  dimkerim  33712  eulerpartgbij  34457  eulerpartlemn  34466  reprpmtf1o  34711  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem28  37761  wessf1ornlem  45345  disjf1o  45351  ssnnf1octb  45354  sge0fodjrnlem  46576  f1oresf1orab  47451  isgrim  48044  isubgrgrim  48091  isgrlim  48144  uspgrlim  48154  grlimedgclnbgr  48157  grlimgrtri  48165  grilcbri2  48173  gpg5grlim  48255  swapf1f1o  49436  swapf2f1o  49437  swapf2f1oa  49438  swapf2f1oaALT  49439  fucoppc  49571