![]() |
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 1129 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7510 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | mptru 1544 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ⊤wtru 1538 ∈ wcel 2106 ∈ cmpo 7433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-oprab 7435 df-mpo 7436 |
This theorem is referenced by: mpodifsnif 7548 mposnif 7549 oprab2co 8121 cnfcomlem 9737 cnfcom2 9740 dfioo2 13487 elovmpowrd 14593 sadcom 16497 comfffval2 17746 oppchomf 17767 symgga 19440 oppglsm 19675 dfrhm2 20491 cnfldsub 21428 cnflddiv 21431 cnflddivOLD 21432 mat0op 22441 mattpos1 22478 mdetunilem7 22640 madufval 22659 maducoeval2 22662 madugsum 22665 mp2pm2mplem5 22832 mp2pm2mp 22833 leordtval 23237 xpstopnlem1 23833 divcnOLD 24904 divcn 24906 oprpiece1res1 24996 oprpiece1res2 24997 ehl1eudis 25468 ehl2eudis 25470 cxpcn 26802 cxpcnOLD 26803 cnnvm 30711 mdetpmtr2 33785 madjusmdetlem1 33788 cnre2csqima 33872 mndpluscn 33887 raddcn 33890 icorempo 37334 matunitlindflem1 37603 mendplusgfval 43170 hoidmv1le 46550 hspdifhsp 46572 vonn0ioo 46643 vonn0icc 46644 dflinc2 48256 |
Copyright terms: Public domain | W3C validator |