Theorem f1eq123d 6840

Description: Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)

Hypotheses

Ref	Expression
f1eq123d.1	⊢ (𝜑 → 𝐹 = 𝐺)
f1eq123d.2	⊢ (𝜑 → 𝐴 = 𝐵)
f1eq123d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
f1eq123d	⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))

Proof of Theorem f1eq123d

Step	Hyp	Ref	Expression
1		f1eq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1eq1 6799	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1eq2 6800	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
6	4, 5	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1eq3 6801	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
9	7, 8	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
10	3, 6, 9	3bitrd 305	1 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  –1-1→wf1 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567

This theorem is referenced by:  f10d  6882  fthf1  17970  cofth  17988  rngqiprngimf1  21327  istrkgld  28481  istrkg2ld  28482  isushgr  29092  isuspgr  29183  isusgr  29184  isuspgrop  29192  isusgrop  29193  ausgrusgrb  29196  ausgrusgri  29199  usgrstrrepe  29266  uspgr1e  29275  usgrres1  29346  usgrexi  29472  uspgr2wlkeq  29678  usgr2trlncl  29792  aciunf1  32679  pfxf1  32910  s1f1  32911  tocycfv  33111  tocycf  33119  tocyc01  33120  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem1  33128  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cycpm3cl2  33138  cycpmconjv  33144  tocyccntz  33146  cyc3evpm  33152  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  dimkerim  33654  f1resfz0f1d  35097  aks6d1c2  42111  f1cof1b  47026  fundcmpsurinjALT  47336  stgrusgra  47861  gpgusgra  47946