![]() |
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 1128 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7488 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | mptru 1546 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1539 ⊤wtru 1540 ∈ wcel 2104 ∈ cmpo 7413 |
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 1911 ax-6 1969 ax-7 2009 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1087 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-oprab 7415 df-mpo 7416 |
This theorem is referenced by: mpodifsnif 7525 mposnif 7526 oprab2co 8085 cnfcomlem 9696 cnfcom2 9699 dfioo2 13431 elovmpowrd 14512 sadcom 16408 comfffval2 17649 oppchomf 17670 symgga 19316 oppglsm 19551 dfrhm2 20365 cnfldsub 21173 cnflddiv 21175 mat0op 22141 mattpos1 22178 mdetunilem7 22340 madufval 22359 maducoeval2 22362 madugsum 22365 mp2pm2mplem5 22532 mp2pm2mp 22533 leordtval 22937 xpstopnlem1 23533 divcnOLD 24604 divcn 24606 oprpiece1res1 24696 oprpiece1res2 24697 ehl1eudis 25168 ehl2eudis 25170 cxpcn 26489 cnnvm 30202 mdetpmtr2 33102 madjusmdetlem1 33105 cnre2csqima 33189 mndpluscn 33204 raddcn 33207 gg-cxpcn 35470 icorempo 36535 matunitlindflem1 36787 mendplusgfval 42229 hoidmv1le 45608 hspdifhsp 45630 vonn0ioo 45701 vonn0icc 45702 dflinc2 47178 |
Copyright terms: Public domain | W3C validator |