![]() |
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 1124 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpt2eq3dva 6876 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | trud 1634 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1624 ⊤wtru 1625 ∈ wcel 2131 ↦ cmpt2 6807 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-oprab 6809 df-mpt2 6810 |
This theorem is referenced by: mpt2difsnif 6910 mpt2snif 6911 oprab2co 7422 cnfcomlem 8761 cnfcom2 8764 dfioo2 12459 elovmpt2wrd 13526 sadcom 15379 comfffval2 16554 oppchomf 16573 symgga 18018 oppglsm 18249 dfrhm2 18911 cnfldsub 19968 cnflddiv 19970 mat0op 20419 mattpos1 20456 mdetunilem7 20618 madufval 20637 maducoeval2 20640 madugsum 20643 mp2pm2mplem5 20809 mp2pm2mp 20810 leordtval 21211 xpstopnlem1 21806 divcn 22864 oprpiece1res1 22943 oprpiece1res2 22944 cxpcn 24677 cnnvm 27838 mdetpmtr2 30191 madjusmdetlem1 30194 cnre2csqima 30258 mndpluscn 30273 raddcn 30276 icorempt2 33502 matunitlindflem1 33710 mendplusgfval 38249 hoidmv1le 41306 hspdifhsp 41328 vonn0ioo 41399 vonn0icc 41400 dflinc2 42701 |
Copyright terms: Public domain | W3C validator |