![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1veqaeq | Structured version Visualization version GIF version |
Description: If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
Ref | Expression |
---|---|
f1veqaeq | ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dff13 6991 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑐 ∈ 𝐴 ∀𝑑 ∈ 𝐴 ((𝐹‘𝑐) = (𝐹‘𝑑) → 𝑐 = 𝑑))) | |
2 | fveqeq2 6654 | . . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝐹‘𝑐) = (𝐹‘𝑑) ↔ (𝐹‘𝐶) = (𝐹‘𝑑))) | |
3 | eqeq1 2802 | . . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 = 𝑑 ↔ 𝐶 = 𝑑)) | |
4 | 2, 3 | imbi12d 348 | . . . . 5 ⊢ (𝑐 = 𝐶 → (((𝐹‘𝑐) = (𝐹‘𝑑) → 𝑐 = 𝑑) ↔ ((𝐹‘𝐶) = (𝐹‘𝑑) → 𝐶 = 𝑑))) |
5 | fveq2 6645 | . . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝐹‘𝑑) = (𝐹‘𝐷)) | |
6 | 5 | eqeq2d 2809 | . . . . . 6 ⊢ (𝑑 = 𝐷 → ((𝐹‘𝐶) = (𝐹‘𝑑) ↔ (𝐹‘𝐶) = (𝐹‘𝐷))) |
7 | eqeq2 2810 | . . . . . 6 ⊢ (𝑑 = 𝐷 → (𝐶 = 𝑑 ↔ 𝐶 = 𝐷)) | |
8 | 6, 7 | imbi12d 348 | . . . . 5 ⊢ (𝑑 = 𝐷 → (((𝐹‘𝐶) = (𝐹‘𝑑) → 𝐶 = 𝑑) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))) |
9 | 4, 8 | rspc2v 3581 | . . . 4 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∀𝑐 ∈ 𝐴 ∀𝑑 ∈ 𝐴 ((𝐹‘𝑐) = (𝐹‘𝑑) → 𝑐 = 𝑑) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))) |
10 | 9 | com12 32 | . . 3 ⊢ (∀𝑐 ∈ 𝐴 ∀𝑑 ∈ 𝐴 ((𝐹‘𝑐) = (𝐹‘𝑑) → 𝑐 = 𝑑) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))) |
11 | 1, 10 | simplbiim 508 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))) |
12 | 11 | imp 410 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ⟶wf 6320 –1-1→wf1 6321 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fv 6332 |
This theorem is referenced by: f1cofveqaeq 6994 f1cofveqaeqALT 6995 2f1fvneq 6996 f1fveq 6998 f1prex 7018 f1ocnvfvrneq 7020 f1o2ndf1 7801 symgfvne 18501 f1ghm0to0 19488 mat2pmatf1 21334 f1otrg 26665 uspgr2wlkeq 27435 pthdivtx 27518 spthdep 27523 spthonepeq 27541 usgr2trlncl 27549 ccatf1 30651 swrdf1 30656 cycpmrn 30835 f1resveqaeq 32468 poimirlem1 35058 poimirlem9 35066 poimirlem22 35079 mblfinlem2 35095 isomuspgrlem1 44345 |
Copyright terms: Public domain | W3C validator |