![]() |
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 1130 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7482 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
4 | 3 | mptru 1548 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ⊤wtru 1542 ∈ wcel 2106 ∈ cmpo 7407 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1089 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-oprab 7409 df-mpo 7410 |
This theorem is referenced by: mpodifsnif 7519 mposnif 7520 oprab2co 8079 cnfcomlem 9690 cnfcom2 9693 dfioo2 13423 elovmpowrd 14504 sadcom 16400 comfffval2 17641 oppchomf 17662 symgga 19269 oppglsm 19504 dfrhm2 20245 cnfldsub 20965 cnflddiv 20967 mat0op 21912 mattpos1 21949 mdetunilem7 22111 madufval 22130 maducoeval2 22133 madugsum 22136 mp2pm2mplem5 22303 mp2pm2mp 22304 leordtval 22708 xpstopnlem1 23304 divcn 24375 oprpiece1res1 24458 oprpiece1res2 24459 ehl1eudis 24928 ehl2eudis 24930 cxpcn 26242 cnnvm 29922 mdetpmtr2 32792 madjusmdetlem1 32795 cnre2csqima 32879 mndpluscn 32894 raddcn 32897 gg-divcn 35151 gg-cxpcn 35172 icorempo 36220 matunitlindflem1 36472 mendplusgfval 41912 hoidmv1le 45296 hspdifhsp 45318 vonn0ioo 45389 vonn0icc 45390 dflinc2 47044 |
Copyright terms: Public domain | W3C validator |