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 1079 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpt2eq3dva 6719 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | trud 1493 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ⊤wtru 1484 ∈ wcel 1990 ↦ cmpt2 6652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-oprab 6654 df-mpt2 6655 |
This theorem is referenced by: mpt2difsnif 6753 mpt2snif 6754 oprab2co 7262 cnfcomlem 8596 cnfcom2 8599 dfioo2 12274 elovmpt2wrd 13347 sadcom 15185 comfffval2 16361 oppchomf 16380 symgga 17826 oppglsm 18057 dfrhm2 18717 cnfldsub 19774 cnflddiv 19776 mat0op 20225 mattpos1 20262 mdetunilem7 20424 madufval 20443 maducoeval2 20446 madugsum 20449 mp2pm2mplem5 20615 mp2pm2mp 20616 leordtval 21017 xpstopnlem1 21612 divcn 22671 oprpiece1res1 22750 oprpiece1res2 22751 cxpcn 24486 numclwwlk6 27248 cnnvm 27537 mdetpmtr2 29890 madjusmdetlem1 29893 cnre2csqima 29957 mndpluscn 29972 raddcn 29975 icorempt2 33199 matunitlindflem1 33405 mendplusgfval 37755 hoidmv1le 40808 hspdifhsp 40830 vonn0ioo 40901 vonn0icc 40902 dflinc2 42199 |
Copyright terms: Public domain | W3C validator |