Theorem mpteq2dva 4123

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167   ↦ cmpt 4094

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-opab 4095  df-mpt 4096

This theorem is referenced by:  mpteq2dv  4124  fmptapd  5753  offval  6143  offval2  6151  caofinvl  6160  caofcom  6161  caofdig  6164  freceq1  6450  freceq2  6451  pw2f1odclem  6895  mapxpen  6909  xpmapenlem  6910  nnnninf2  7193  nninfwlpoimlemginf  7242  fser0const  10627  sumeq1  11520  sumeq2  11524  prodeq2  11722  prod1dc  11751  restid2  12919  qusin  12969  grpinvpropdg  13207  mulgrhm2  14166  cnmpt1t  14521  cnmpt12  14523  fsumcncntop  14803  expcn  14805  divccncfap  14826  cdivcncfap  14840  expcncf  14845  divcncfap  14850  maxcncf  14851  mincncf  14852  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvimulf  14942  dvcoapbr  14943  dvcjbr  14944  dvcj  14945  dvfre  14946  dvexp  14947  dvexp2  14948  dvrecap  14949  dvmptcmulcn  14957  dvmptnegcn  14958  dvmptsubcn  14959  dvmptfsum  14961  dvef  14963  ply1termlem  14978  plypow  14980  plyconst  14981  plyaddlem1  14983  plymullem1  14984  plycolemc  14994  plycjlemc  14996  dvply1  15001  dvply2g  15002  lgsval4lem  15252  lgsneg  15265  lgsmod  15267  lgseisenlem3  15313  lgseisenlem4  15314