| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ovmpod | Structured version Visualization version GIF version | ||
| Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| Ref | Expression |
|---|---|
| ovmpod.1 | ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) |
| ovmpod.2 | ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) |
| ovmpod.3 | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| ovmpod.4 | ⊢ (𝜑 → 𝐵 ∈ 𝐷) |
| ovmpod.5 | ⊢ (𝜑 → 𝑆 ∈ 𝑋) |
| Ref | Expression |
|---|---|
| ovmpod | ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovmpod.1 | . 2 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) | |
| 2 | ovmpod.2 | . 2 ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) | |
| 3 | eqidd 2738 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐷) | |
| 4 | ovmpod.3 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶) | |
| 5 | ovmpod.4 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷) | |
| 6 | ovmpod.5 | . 2 ⊢ (𝜑 → 𝑆 ∈ 𝑋) | |
| 7 | 1, 2, 3, 4, 5, 6 | ovmpodx 7584 | 1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |
| Copyright terms: Public domain | W3C validator |