| 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 1131 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
| 3 | 2 | mpoeq3dva 7510 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
| 4 | 3 | mptru 1547 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2108 ∈ cmpo 7433 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: mpodifsnif 7548 mposnif 7549 oprab2co 8122 cnfcomlem 9739 cnfcom2 9742 dfioo2 13490 elovmpowrd 14596 sadcom 16500 comfffval2 17744 oppchomf 17763 symgga 19425 oppglsm 19660 dfrhm2 20474 cnfldsub 21410 cnflddiv 21413 cnflddivOLD 21414 mat0op 22425 mattpos1 22462 mdetunilem7 22624 madufval 22643 maducoeval2 22646 madugsum 22649 mp2pm2mplem5 22816 mp2pm2mp 22817 leordtval 23221 xpstopnlem1 23817 divcnOLD 24890 divcn 24892 oprpiece1res1 24982 oprpiece1res2 24983 ehl1eudis 25454 ehl2eudis 25456 cxpcn 26787 cxpcnOLD 26788 cnnvm 30701 mdetpmtr2 33823 madjusmdetlem1 33826 cnre2csqima 33910 mndpluscn 33925 raddcn 33928 icorempo 37352 matunitlindflem1 37623 mendplusgfval 43193 hoidmv1le 46609 hspdifhsp 46631 vonn0ioo 46702 vonn0icc 46703 dflinc2 48327 dfswapf2 48967 |
| Copyright terms: Public domain | W3C validator |