Theorem f1oeq123d 6761

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1oprswap  6812  f1oprg  6813  f1ossf1o  7070  cnfcom  9612  ackbij2lem2  10152  idffth  17893  ressffth  17898  symgval  19337  symg1bas  19357  symg2bas  19359  symgfixels  19400  symgfixelsi  19401  rnghmf1o  20423  rhmf1o  20462  mat1f1o  22461  ushgredgedg  29316  ushgredgedgloop  29318  trlreslem  29784  wlknwwlksnbij  29974  wwlksnextbij  29988  clwlknf1oclwwlkn  30172  eupth0  30302  eupthp1  30304  foresf1o  32592  f1ocnt  32892  indf1ofs  32945  gsumwrd2dccat  33159  symgcom  33164  cycpmcl  33197  cycpmconjslem2  33236  nsgqusf1o  33499  1arithidomlem2  33619  1arithidom  33620  dimkerim  33811  eulerpartgbij  34556  eulerpartlemn  34565  reprpmtf1o  34810  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem28  38015  wessf1ornlem  45632  disjf1o  45638  ssnnf1octb  45641  sge0fodjrnlem  46859  f1oresf1orab  47752  isgrim  48373  isubgrgrim  48420  isgrlim  48473  uspgrlim  48483  grlimedgclnbgr  48486  grlimgrtri  48494  grilcbri2  48502  gpg5grlim  48584  swapf1f1o  49765  swapf2f1o  49766  swapf2f1oa  49767  swapf2f1oaALT  49768  fucoppc  49900