![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpteq2dva | GIF version |
Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Ref | Expression |
---|---|
mpteq2dva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
mpteq2dva | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1528 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | mpteq2dva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) | |
3 | 1, 2 | mpteq2da 4092 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∈ wcel 2148 ↦ cmpt 4064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-ral 2460 df-opab 4065 df-mpt 4066 |
This theorem is referenced by: mpteq2dv 4094 fmptapd 5707 offval 6089 offval2 6097 caofinvl 6104 caofcom 6105 freceq1 6392 freceq2 6393 mapxpen 6847 xpmapenlem 6848 nnnninf2 7124 nninfwlpoimlemginf 7173 fser0const 10513 sumeq1 11358 sumeq2 11362 prodeq2 11560 prod1dc 11589 restid2 12691 qusin 12740 grpinvpropdg 12939 cnmpt1t 13716 cnmpt12 13718 fsumcncntop 13987 divccncfap 14008 cdivcncfap 14018 expcncf 14023 dvidlemap 14091 dvcnp2cntop 14094 dvaddxxbr 14096 dvmulxxbr 14097 dvimulf 14101 dvcoapbr 14102 dvcjbr 14103 dvcj 14104 dvfre 14105 dvexp 14106 dvexp2 14107 dvrecap 14108 dvmptcmulcn 14114 dvmptnegcn 14115 dvmptsubcn 14116 dvef 14119 lgsval4lem 14343 lgsneg 14356 lgsmod 14358 |
Copyright terms: Public domain | W3C validator |