![]() |
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 6781 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐴–1-1→𝐶)) |
4 | f1eq123d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
5 | f1eq2 6782 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶)) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐶)) |
7 | f1eq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
8 | f1eq3 6783 | . . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷)) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐵–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷)) |
10 | 3, 6, 9 | 3bitrd 304 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 –1-1→wf1 6539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 |
This theorem is referenced by: f10d 6866 fthf1 17872 cofth 17890 rngqiprngimf1 21059 istrkgld 27977 istrkg2ld 27978 isushgr 28588 isuspgr 28679 isusgr 28680 isuspgrop 28688 isusgrop 28689 ausgrusgrb 28692 ausgrusgri 28695 usgrstrrepe 28759 uspgr1e 28768 usgrexmpl 28787 usgrres1 28839 usgrexi 28965 uspgr2wlkeq 29170 usgr2trlncl 29284 aciunf1 32155 pfxf1 32375 s1f1 32376 tocycfv 32538 tocycf 32546 tocyc01 32547 cycpmco2f1 32553 cycpmco2rn 32554 cycpmco2lem1 32555 cycpmco2lem2 32556 cycpmco2lem3 32557 cycpmco2lem4 32558 cycpmco2lem5 32559 cycpmco2lem6 32560 cycpmco2lem7 32561 cycpmco2 32562 cycpm3cl2 32565 cycpmconjv 32571 tocyccntz 32573 cyc3evpm 32579 cycpmgcl 32582 cycpmconjslem2 32584 cyc3conja 32586 dimkerim 33000 f1resfz0f1d 34401 f1cof1b 46083 fundcmpsurinjALT 46378 |
Copyright terms: Public domain | W3C validator |