Theorem mpt2eq123dv 6944

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)

Hypotheses

Ref	Expression
mpt2eq123dv.1	⊢ (𝜑 → 𝐴 = 𝐷)
mpt2eq123dv.2	⊢ (𝜑 → 𝐵 = 𝐸)
mpt2eq123dv.3	⊢ (𝜑 → 𝐶 = 𝐹)

Assertion

Ref	Expression
mpt2eq123dv	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpt2eq123dv

Step	Hyp	Ref	Expression
1		mpt2eq123dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
2		mpt2eq123dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐸)
3	2	adantr 468	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
4		mpt2eq123dv.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐹)
5	4	adantr 468	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
6	1, 3, 5	mpt2eq123dva 6943	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2158   ↦ cmpt2 6873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-oprab 6875  df-mpt2 6876

This theorem is referenced by:  mpt2eq123i  6945  mptmpt2opabbrd  7478  el2mpt2csbcl  7480  bropopvvv  7486  bropfvvvv  7488  prdsval  16316  imasval  16372  imasvscaval  16399  homffval  16550  homfeq  16554  comfffval  16558  comffval  16559  comfffval2  16561  comffval2  16562  comfeq  16566  oppcval  16573  monfval  16592  sectffval  16610  invffval  16618  isofn  16635  cofuval  16742  natfval  16806  fucval  16818  fucco  16822  coafval  16914  setcval  16927  setcco  16933  catcval  16946  catcco  16951  estrcval  16964  estrcco  16970  xpcval  17018  xpchomfval  17020  xpccofval  17023  1stfval  17032  2ndfval  17035  prfval  17040  evlfval  17058  evlf2  17059  curfval  17064  hofval  17093  hof2fval  17096  plusffval  17448  grpsubfval  17665  grpsubpropd  17721  mulgfval  17743  mulgpropd  17782  symgval  17996  lsmfval  18250  pj1fval  18304  efgtf  18332  prdsmgp  18808  dvrfval  18882  scaffval  19081  psrval  19567  ipffval  20199  phssip  20209  frlmip  20323  mamufval  20397  mvmulfval  20555  marrepfval  20573  marepvfval  20578  submafval  20592  submaval  20594  madufval  20650  minmar1fval  20659  mat2pmatfval  20737  cpm2mfval  20763  decpmatval0  20778  decpmatval  20779  pmatcollpw3lem  20797  xkoval  21600  xkopt  21668  xpstopnlem1  21822  submtmd  22117  blfvalps  22397  ishtpy  22980  isphtpy  22989  pcofval  23018  rrxip  23386  q1pval  24123  r1pval  24126  taylfval  24323  midf  25878  ismidb  25880  ttgval  25965  wwlksnon  26969  wspthsnon  26970  clwwlknonmpt2  27250  grpodivfval  27713  dipfval  27882  submatres  30194  lmatval  30201  lmatcl  30204  qqhval  30340  sxval  30575  sitmval  30733  cndprobval  30817  mclsval  31780  csbfinxpg  33538  rrnval  33934  ldualset  34902  paddfval  35574  tgrpfset  36522  tgrpset  36523  erngfset  36577  erngset  36578  erngfset-rN  36585  erngset-rN  36586  dvafset  36782  dvaset  36783  dvhfset  36858  dvhset  36859  djaffvalN  36911  djafvalN  36912  djhffval  37174  djhfval  37175  hlhilset  37712  eldiophb  37819  mendval  38251  hoidmvval  41270  ovnhoi  41296  hspval  41302  hspmbllem2  41320  hoimbl  41324  rngcvalALTV  42526  rngccoALTV  42553  funcrngcsetcALT  42564  ringcvalALTV  42572  ringccoALTV  42616  lincop  42762