Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpoeq3ia | Structured version Visualization version GIF version |
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpoeq3ia.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
mpoeq3ia | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoeq3ia.1 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) | |
2 | 1 | 3adant1 1126 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7231 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | mptru 1544 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ∈ cmpo 7158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2124 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-oprab 7160 df-mpo 7161 |
This theorem is referenced by: mpodifsnif 7267 mposnif 7268 oprab2co 7792 cnfcomlem 9162 cnfcom2 9165 dfioo2 12839 elovmpowrd 13910 sadcom 15812 comfffval2 16971 oppchomf 16990 symgga 18535 oppglsm 18767 dfrhm2 19469 cnfldsub 20573 cnflddiv 20575 mat0op 21028 mattpos1 21065 mdetunilem7 21227 madufval 21246 maducoeval2 21249 madugsum 21252 mp2pm2mplem5 21418 mp2pm2mp 21419 leordtval 21821 xpstopnlem1 22417 divcn 23476 oprpiece1res1 23555 oprpiece1res2 23556 ehl1eudis 24023 ehl2eudis 24025 cxpcn 25326 cnnvm 28459 mdetpmtr2 31089 madjusmdetlem1 31092 cnre2csqima 31154 mndpluscn 31169 raddcn 31172 icorempo 34635 matunitlindflem1 34903 mendplusgfval 39805 hoidmv1le 42896 hspdifhsp 42918 vonn0ioo 42989 vonn0icc 42990 dflinc2 44485 |
Copyright terms: Public domain | W3C validator |