| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mpteq12dv | GIF version | ||
| Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
| Ref | Expression |
|---|---|
| mpteq12dv.1 | ⊢ (𝜑 → 𝐴 = 𝐶) |
| mpteq12dv.2 | ⊢ (𝜑 → 𝐵 = 𝐷) |
| Ref | Expression |
|---|---|
| mpteq12dv | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpteq12dv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
| 2 | mpteq12dv.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
| 3 | 2 | adantr 276 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) |
| 4 | 1, 3 | mpteq12dva 4193 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1398 ∈ wcel 2205 ↦ cmpt 4173 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-11 1555 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2216 |
| This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2221 df-cleq 2227 df-clel 2230 df-ral 2527 df-opab 4174 df-mpt 4175 |
| This theorem is referenced by: mpteq12i 4200 offval 6276 offval3 6329 ccatfvalfi 11284 swrdval 11344 odzval 12943 restval 13475 prdsex 13499 prdsval 13503 qusval 13553 grpinvfvalg 13772 grpinvpropdg 13805 opprnegg 14244 lspfval 14553 lsppropd 14597 sraval 14602 psrval 14831 ntrfval 14982 clsfval 14983 neifval 15022 cnpfval 15077 cnprcl2k 15088 reldvg 15561 dvfvalap 15563 eldvap 15564 vtxdgfval 16300 vtxdgop 16304 vtxdeqd 16308 |
| Copyright terms: Public domain | W3C validator |