![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ovmpt2ga | GIF version |
Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Ref | Expression |
---|---|
ovmpt2ga.1 | ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) |
ovmpt2ga.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
Ref | Expression |
---|---|
ovmpt2ga | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2619 | . 2 ⊢ (𝑆 ∈ 𝐻 → 𝑆 ∈ V) | |
2 | ovmpt2ga.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) | |
3 | 2 | a1i 9 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) |
4 | ovmpt2ga.1 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) | |
5 | 4 | adantl 271 | . . 3 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) |
6 | simp1 939 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐴 ∈ 𝐶) | |
7 | simp2 940 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐵 ∈ 𝐷) | |
8 | simp3 941 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝑆 ∈ V) | |
9 | 3, 5, 6, 7, 8 | ovmpt2d 5679 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
10 | 1, 9 | syl3an3 1205 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 = wceq 1285 ∈ wcel 1434 Vcvv 2610 (class class class)co 5563 ↦ cmpt2 5565 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3916 ax-pow 3968 ax-pr 3992 ax-setind 4308 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-ral 2358 df-rex 2359 df-v 2612 df-sbc 2825 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-br 3806 df-opab 3860 df-id 4076 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-iota 4917 df-fun 4954 df-fv 4960 df-ov 5566 df-oprab 5567 df-mpt2 5568 |
This theorem is referenced by: ovmpt2a 5682 ovmpt2g 5686 elovmpt2 5752 offval 5770 offval3 5812 fzoval 9287 eucalgval2 10642 |
Copyright terms: Public domain | W3C validator |