![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1eq123d | Structured version Visualization version GIF version |
Description: Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Ref | Expression |
---|---|
f1eq123d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
f1eq123d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
f1eq123d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
f1eq123d | ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq123d.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | f1eq1 6783 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶)) |
4 | f1eq123d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
5 | f1eq2 6784 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶)) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶)) |
7 | f1eq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
8 | f1eq3 6785 | . . 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→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 –1-1→wf1 6541 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 |
This theorem is referenced by: f10d 6868 fthf1 17868 cofth 17886 istrkgld 27710 istrkg2ld 27711 isushgr 28321 isuspgr 28412 isusgr 28413 isuspgrop 28421 isusgrop 28422 ausgrusgrb 28425 ausgrusgri 28428 usgrstrrepe 28492 uspgr1e 28501 usgrexmpl 28520 usgrres1 28572 usgrexi 28698 uspgr2wlkeq 28903 usgr2trlncl 29017 aciunf1 31888 pfxf1 32108 s1f1 32109 tocycfv 32268 tocycf 32276 tocyc01 32277 cycpmco2f1 32283 cycpmco2rn 32284 cycpmco2lem1 32285 cycpmco2lem2 32286 cycpmco2lem3 32287 cycpmco2lem4 32288 cycpmco2lem5 32289 cycpmco2lem6 32290 cycpmco2lem7 32291 cycpmco2 32292 cycpm3cl2 32295 cycpmconjv 32301 tocyccntz 32303 cyc3evpm 32309 cycpmgcl 32312 cycpmconjslem2 32314 cyc3conja 32316 dimkerim 32712 f1resfz0f1d 34103 f1cof1b 45785 fundcmpsurinjALT 46080 rngqiprngimf1 46785 |
Copyright terms: Public domain | W3C validator |