Theorem mpteq2dva 4072

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 1516	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4071	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343   ∈ wcel 2136   ↦ cmpt 4043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-ral 2449  df-opab 4044  df-mpt 4045

This theorem is referenced by:  mpteq2dv  4073  fmptapd  5676  offval  6057  offval2  6065  caofinvl  6072  caofcom  6073  freceq1  6360  freceq2  6361  mapxpen  6814  xpmapenlem  6815  nnnninf2  7091  fser0const  10451  sumeq1  11296  sumeq2  11300  prodeq2  11498  prod1dc  11527  restid2  12565  cnmpt1t  12925  cnmpt12  12927  fsumcncntop  13196  divccncfap  13217  cdivcncfap  13227  expcncf  13232  dvidlemap  13300  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvimulf  13310  dvcoapbr  13311  dvcjbr  13312  dvcj  13313  dvfre  13314  dvexp  13315  dvexp2  13316  dvrecap  13317  dvmptcmulcn  13323  dvmptnegcn  13324  dvmptsubcn  13325  dvef  13328  lgsval4lem  13552  lgsneg  13565  lgsmod  13567