Theorem f1eq123d 6701

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 6658	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1eq2 6659	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
6	4, 5	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1eq3 6660	. . 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 6424

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 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5075  df-opab 5137  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-fun 6429  df-fn 6430  df-f 6431  df-f1 6432

This theorem is referenced by:  f10d  6743  fthf1  17621  cofth  17639  istrkgld  26808  istrkg2ld  26809  isushgr  27419  isuspgr  27510  isusgr  27511  isuspgrop  27519  isusgrop  27520  ausgrusgrb  27523  ausgrusgri  27526  usgrstrrepe  27590  uspgr1e  27599  usgrexmpl  27618  usgrres1  27670  usgrexi  27796  uspgr2wlkeq  28000  usgr2trlncl  28114  aciunf1  30986  pfxf1  31202  s1f1  31203  tocycfv  31362  tocycf  31370  tocyc01  31371  cycpmco2f1  31377  cycpmco2rn  31378  cycpmco2lem1  31379  cycpmco2lem2  31380  cycpmco2lem3  31381  cycpmco2lem4  31382  cycpmco2lem5  31383  cycpmco2lem6  31384  cycpmco2lem7  31385  cycpmco2  31386  cycpm3cl2  31389  cycpmconjv  31395  tocyccntz  31397  cyc3evpm  31403  cycpmgcl  31406  cycpmconjslem2  31408  cyc3conja  31410  dimkerim  31694  f1resfz0f1d  33058  f1cof1b  44525  fundcmpsurinjALT  44820