Theorem mpteq2dva 4079

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348   ∈ wcel 2141   ↦ cmpt 4050

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-ral 2453  df-opab 4051  df-mpt 4052

This theorem is referenced by:  mpteq2dv  4080  fmptapd  5687  offval  6068  offval2  6076  caofinvl  6083  caofcom  6084  freceq1  6371  freceq2  6372  mapxpen  6826  xpmapenlem  6827  nnnninf2  7103  nninfwlpoimlemginf  7152  fser0const  10472  sumeq1  11318  sumeq2  11322  prodeq2  11520  prod1dc  11549  restid2  12588  cnmpt1t  13079  cnmpt12  13081  fsumcncntop  13350  divccncfap  13371  cdivcncfap  13381  expcncf  13386  dvidlemap  13454  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvimulf  13464  dvcoapbr  13465  dvcjbr  13466  dvcj  13467  dvfre  13468  dvexp  13469  dvexp2  13470  dvrecap  13471  dvmptcmulcn  13477  dvmptnegcn  13478  dvmptsubcn  13479  dvef  13482  lgsval4lem  13706  lgsneg  13719  lgsmod  13721