![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovmpt4g | Structured version Visualization version GIF version |
Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 6959.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
ovmpt4g.3 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
ovmpt4g | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2819 | . . 3 ⊢ (𝐶 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐶) | |
2 | moeq 3665 | . . . . . . 7 ⊢ ∃*𝑧 𝑧 = 𝐶 | |
3 | 2 | a1i 11 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧 𝑧 = 𝐶) |
4 | ovmpt4g.3 | . . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
5 | df-mpo 7362 | . . . . . . 7 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
6 | 4, 5 | eqtri 2764 | . . . . . 6 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
7 | 3, 6 | ovidi 7498 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝑧)) |
8 | eqeq2 2748 | . . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑥𝐹𝑦) = 𝑧 ↔ (𝑥𝐹𝑦) = 𝐶)) | |
9 | 7, 8 | mpbidi 240 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶)) |
10 | 9 | exlimdv 1936 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶)) |
11 | 1, 10 | syl5 34 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐶 ∈ 𝑉 → (𝑥𝐹𝑦) = 𝐶)) |
12 | 11 | 3impia 1117 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ∃*wmo 2536 (class class class)co 7357 {coprab 7358 ∈ cmpo 7359 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 |
This theorem is referenced by: ovmpos 7503 ov2gf 7504 ovmpodxf 7505 ovmpodf 7511 ofmres 7917 fnmpoovd 8019 mapxpen 9087 pwfseqlem2 10595 pwfseqlem3 10596 fullfunc 17793 fthfunc 17794 prfcl 18091 curf1cl 18117 curfcl 18121 hofcl 18148 gsum2d2lem 19750 gsum2d2 19751 gsumcom2 19752 dprdval 19782 dprd2d2 19823 cnmpt21 23022 cnmpt2t 23024 cnmptcom 23029 cnmpt2k 23039 xkocnv 23165 suppovss 31598 fedgmullem1 32324 fedgmullem2 32325 fedgmul 32326 madjusmdetlem1 32408 madjusmdetlem3 32410 finxpreclem5 35866 sdclem2 36201 smflimlem1 45002 smflimlem2 45003 aovmpt4g 45423 ovmpordxf 46404 |
Copyright terms: Public domain | W3C validator |