Theorem f1oeq123d 6789

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 6783	. . 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 6784	. . 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 6785	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 307	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554  –1-1-onto→wf1o 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-opab 5157  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517

This theorem is referenced by:  f1oprswap  6841  f1oprg  6842  f1ossf1o  7099  cnfcom  9645  ackbij2lem2  10185  idffth  17944  ressffth  17949  symgval  19387  symg1bas  19407  symg2bas  19409  symgfixels  19450  symgfixelsi  19451  rnghmf1o  20473  rhmf1o  20512  mat1f1o  22511  ushgredgedg  29369  ushgredgedgloop  29371  trlreslem  29837  wlknwwlksnbij  30027  wwlksnextbij  30041  clwlknf1oclwwlkn  30225  eupth0  30355  eupthp1  30357  foresf1o  32645  f1ocnt  32945  indf1ofs  32998  gsumwrd2dccat  33212  symgcom  33217  cycpmcl  33250  cycpmconjslem2  33289  nsgqusf1o  33556  1arithidomlem2  33686  1arithidom  33687  dimkerim  33878  eulerpartgbij  34623  eulerpartlemn  34632  reprpmtf1o  34877  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem28  38095  wessf1ornlem  45711  disjf1o  45717  ssnnf1octb  45720  sge0fodjrnlem  46938  f1oresf1orab  47831  isgrim  48452  isubgrgrim  48499  isgrlim  48552  uspgrlim  48562  grlimedgclnbgr  48565  grlimgrtri  48573  grilcbri2  48581  gpg5grlim  48663  swapf1f1o  49844  swapf2f1o  49845  swapf2f1oa  49846  swapf2f1oaALT  49847  fucoppc  49979