Theorem f1oeq123d 6812

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 6806	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
3	1, 2	syl 18	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1oeq2 6807	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
6	4, 5	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1oeq3 6808	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 308	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:  f1oprswap  6864  f1oprg  6865  f1ossf1o  7122  cnfcom  9665  ackbij2lem2  10218  idffth  17988  ressffth  17993  symgval  19437  symg1bas  19457  symg2bas  19459  symgfixels  19500  symgfixelsi  19501  rnghmf1o  20530  rhmf1o  20569  mat1f1o  22600  ushgredgedg  29516  ushgredgedgloop  29518  trlreslem  29984  wlknwwlksnbij  30174  wwlksnextbij  30188  clwlknf1oclwwlkn  30372  eupth0  30502  eupthp1  30504  foresf1o  32787  f1ocnt  33082  indf1ofs  33123  gsumwrd2dccat  33335  symgcom  33340  cycpmcl  33373  cycpmconjslem2  33412  nsgqusf1o  33665  1arithidomlem2  33767  1arithidom  33768  dimkerim  33958  eulerpartgbij  34703  eulerpartlemn  34712  reprpmtf1o  34954  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem28  38182  wessf1ornlem  45790  disjf1o  45796  ssnnf1octb  45799  sge0fodjrnlem  47017  f1oresf1orab  47910  isgrim  48531  isubgrgrim  48578  isgrlim  48631  uspgrlim  48641  grlimedgclnbgr  48644  grlimgrtri  48652  grilcbri2  48660  gpg5grlim  48742  swapf1f1o  49933  swapf2f1o  49934  swapf2f1oa  49935  swapf2f1oaALT  49936  fucoppc  50068