Theorem f1eq123d 6708

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 6665	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1eq2 6666	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
6	4, 5	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1eq3 6667	. . 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 205   = wceq 1539  –1-1→wf1 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438

This theorem is referenced by:  f10d  6750  fthf1  17633  cofth  17651  istrkgld  26820  istrkg2ld  26821  isushgr  27431  isuspgr  27522  isusgr  27523  isuspgrop  27531  isusgrop  27532  ausgrusgrb  27535  ausgrusgri  27538  usgrstrrepe  27602  uspgr1e  27611  usgrexmpl  27630  usgrres1  27682  usgrexi  27808  uspgr2wlkeq  28013  usgr2trlncl  28128  aciunf1  31000  pfxf1  31216  s1f1  31217  tocycfv  31376  tocycf  31384  tocyc01  31385  cycpmco2f1  31391  cycpmco2rn  31392  cycpmco2lem1  31393  cycpmco2lem2  31394  cycpmco2lem3  31395  cycpmco2lem4  31396  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2lem7  31399  cycpmco2  31400  cycpm3cl2  31403  cycpmconjv  31409  tocyccntz  31411  cyc3evpm  31417  cycpmgcl  31420  cycpmconjslem2  31422  cyc3conja  31424  dimkerim  31708  f1resfz0f1d  33072  f1cof1b  44569  fundcmpsurinjALT  44864