Theorem f1oeq123d 6811

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 6805	. . 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 6806	. . 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 6807	. . 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→𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  –1-1-onto→wf1o 6532

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1oprswap  6863  f1oprg  6864  f1ossf1o  7122  cnfcom  9679  ackbij2lem2  10241  idffth  18024  ressffth  18029  symgval  19498  symg1bas  19518  symg2bas  19520  symgfixels  19561  symgfixelsi  19562  rnghmf1o  20593  rhmf1o  20638  mat1f1o  22700  ushgredgedg  29689  ushgredgedgloop  29691  trlreslem  30161  wlknwwlksnbij  30356  wwlksnextbij  30370  clwlknf1oclwwlkn  30554  eupth0  30694  eupthp1  30696  foresf1o  32979  f1ocnt  33271  indf1ofs  33312  gsumwrd2dccat  33518  symgcom  33523  cycpmcl  33556  cycpmconjslem2  33595  nsgqusf1o  33845  1arithidomlem2  33946  1arithidom  33947  dimkerim  34137  eulerpartgbij  34883  eulerpartlemn  34892  reprpmtf1o  35134  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem28  38397  wessf1ornlem  46017  disjf1o  46023  ssnnf1octb  46026  sge0fodjrnlem  47244  f1oresf1orab  48177  isgrim  48798  isubgrgrim  48845  isgrlim  48898  uspgrlim  48908  grlimedgclnbgr  48911  grlimgrtri  48919  grilcbri2  48927  gpg5grlim  49009  swapf1f1o  50201  swapf2f1o  50202  swapf2f1oa  50203  swapf2f1oaALT  50204  fucoppc  50336