![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovmpoga | Structured version Visualization version GIF version |
Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Ref | Expression |
---|---|
ovmpoga.1 | ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) |
ovmpoga.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
Ref | Expression |
---|---|
ovmpoga | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3485 | . 2 ⊢ (𝑆 ∈ 𝐻 → 𝑆 ∈ V) | |
2 | ovmpoga.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) | |
3 | 2 | a1i 11 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) |
4 | ovmpoga.1 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) | |
5 | 4 | adantl 481 | . . 3 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) |
6 | simp1 1133 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐴 ∈ 𝐶) | |
7 | simp2 1134 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐵 ∈ 𝐷) | |
8 | simp3 1135 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝑆 ∈ V) | |
9 | 3, 5, 6, 7, 8 | ovmpod 7552 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
10 | 1, 9 | syl3an3 1162 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 Vcvv 3466 (class class class)co 7401 ∈ cmpo 7403 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6485 df-fun 6535 df-fv 6541 df-ov 7404 df-oprab 7405 df-mpo 7406 |
This theorem is referenced by: ovmpoa 7555 ovmpog 7559 elovmpo 7644 offval 7672 offval3 7962 mptmpoopabbrdOLDOLD 8063 bropopvvv 8070 reps 14717 hashbcval 16934 setsvalg 17098 ressval 17175 restval 17371 sylow1lem4 19511 sylow3lem2 19538 sylow3lem3 19539 lsmvalx 19549 mvrfval 21850 opsrval 21911 marrepfval 22384 marrepval0 22385 marepvfval 22389 marepvval0 22390 cnmpt12 23493 cnmpt22 23500 qtopval 23521 flimval 23789 fclsval 23834 ucnval 24104 stdbdmetval 24345 fldgenval 32868 resvval 32907 irngval 33229 minplyval 33246 ofcfval3 33589 fmulcl 44782 |
Copyright terms: Public domain | W3C validator |