Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpt2eq3ia | Structured version Visualization version GIF version |
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpt2eq3ia.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
mpt2eq3ia | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpt2eq3ia.1 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) | |
2 | 1 | 3adant1 1072 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpt2eq3dva 6617 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | trud 1484 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ⊤wtru 1476 ∈ wcel 1977 ↦ cmpt2 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-oprab 6553 df-mpt2 6554 |
This theorem is referenced by: mpt2difsnif 6651 mpt2snif 6652 oprab2co 7149 cnfcomlem 8479 cnfcom2 8482 dfioo2 12145 elovmpt2wrd 13202 sadcom 15023 comfffval2 16184 oppchomf 16203 symgga 17649 oppglsm 17880 dfrhm2 18540 cnfldsub 19593 cnflddiv 19595 mat0op 20044 mattpos1 20081 mdetunilem7 20243 madufval 20262 maducoeval2 20265 madugsum 20268 mp2pm2mplem5 20434 mp2pm2mp 20435 leordtval 20827 xpstopnlem1 21422 divcn 22479 oprpiece1res1 22558 oprpiece1res2 22559 cxpcn 24286 wwlknprop 26214 numclwwlk5 26639 numclwwlk7 26641 cnnvm 26921 mdetpmtr2 29218 madjusmdetlem1 29221 cnre2csqima 29285 mndpluscn 29300 raddcn 29303 icorempt2 32375 matunitlindflem1 32575 mendplusgfval 36774 hoidmv1le 39484 hspdifhsp 39506 vonn0ioo 39578 vonn0icc 39579 av-numclwwlk5 41542 av-numclwwlk6 41544 dflinc2 41993 |
Copyright terms: Public domain | W3C validator |