Theorem f1oeq123d 6848

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-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐷))

Proof of Theorem f1oeq123d

Step	Hyp	Ref	Expression
1		f1eq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1oeq1 6842	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐴⟶1-1onto𝐶))
3	1, 2	syl 18	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐴⟶1-1onto𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1oeq2 6843	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐶))
6	4, 5	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1oeq3 6844	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐷))
9	7, 8	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐵⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐷))
10	3, 6, 9	3bitrd 308	1 ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1oprswap  6901  f1oprg  6902  f1ossf1o  7161  cnfcom  9738  ackbij2lem2  10356  idffth  18160  ressffth  18165  symgval  19636  symg1bas  19656  symg2bas  19658  symgfixels  19699  symgfixelsi  19700  rnghmf1o  20733  rhmf1o  20778  mat1f1o  22848  ushgredgedg  29867  ushgredgedgloop  29869  trlreslem  30339  wlknwwlksnbij  30534  wwlksnextbij  30548  clwlknf1oclwwlkn  30732  eupth0  30872  eupthp1  30874  foresf1o  33199  f1ocnt  33488  indf1ofs  33529  gsumwrd2dccat  33738  symgcom  33743  cycpmcl  33776  cycpmconjslem2  33815  nsgqusf1o  34071  1arithidomlem2  34172  1arithidom  34173  dimkerim  34370  eulerpartgbij  35115  eulerpartlemn  35124  reprpmtf1o  35366  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem28  38834  wessf1ornlem  46473  disjf1o  46479  ssnnf1octb  46482  sge0fodjrnlem  47699  f1oresf1orab  48632  isgrim  49253  isubgrgrim  49300  isgrlim  49353  uspgrlim  49363  grlimedgclnbgr  49366  grlimgrtri  49374  grilcbri2  49382  gpg5grlim  49464  swapf1f1o  50728  swapf2f1o  50729  swapf2f1oa  50730  swapf2f1oaALT  50731  fucoppc  50876