Theorem mpteq2dva 4094

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)

Hypothesis

Ref	Expression
mpteq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4093	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148   ↦ cmpt 4065

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 4066  df-mpt 4067

This theorem is referenced by:  mpteq2dv  4095  fmptapd  5708  offval  6090  offval2  6098  caofinvl  6105  caofcom  6106  freceq1  6393  freceq2  6394  mapxpen  6848  xpmapenlem  6849  nnnninf2  7125  nninfwlpoimlemginf  7174  fser0const  10516  sumeq1  11363  sumeq2  11367  prodeq2  11565  prod1dc  11594  restid2  12697  qusin  12746  grpinvpropdg  12945  cnmpt1t  13788  cnmpt12  13790  fsumcncntop  14059  divccncfap  14080  cdivcncfap  14090  expcncf  14095  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvimulf  14173  dvcoapbr  14174  dvcjbr  14175  dvcj  14176  dvfre  14177  dvexp  14178  dvexp2  14179  dvrecap  14180  dvmptcmulcn  14186  dvmptnegcn  14187  dvmptsubcn  14188  dvef  14191  lgsval4lem  14415  lgsneg  14428  lgsmod  14430