Theorem mpt2eq123dv 6996

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 474	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
4		mpt2eq123dv.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐹)
5	4	adantr 474	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
6	1, 3, 5	mpt2eq123dva 6995	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ↦ cmpt2 6926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-oprab 6928  df-mpt2 6929

This theorem is referenced by:  mpt2eq123i  6997  mptmpt2opabbrd  7530  el2mpt2csbcl  7532  bropopvvv  7538  bropfvvvv  7540  prdsval  16505  imasval  16561  imasvscaval  16588  homffval  16739  homfeq  16743  comfffval  16747  comffval  16748  comfffval2  16750  comffval2  16751  comfeq  16755  oppcval  16762  monfval  16781  sectffval  16799  invffval  16807  isofn  16824  cofuval  16931  natfval  16995  fucval  17007  fucco  17011  coafval  17103  setcval  17116  setcco  17122  catcval  17135  catcco  17140  estrcval  17153  estrcco  17159  xpcval  17207  xpchomfval  17209  xpccofval  17212  1stfval  17221  2ndfval  17224  prfval  17229  evlfval  17247  evlf2  17248  curfval  17253  hofval  17282  hof2fval  17285  plusffval  17637  grpsubfval  17855  grpsubpropd  17911  mulgfval  17933  mulgpropd  17972  symgval  18186  lsmfval  18441  pj1fval  18495  efgtf  18523  prdsmgp  19001  dvrfval  19075  scaffval  19277  psrval  19763  ipffval  20395  phssip  20405  frlmip  20525  mamufval  20599  mvmulfval  20757  marrepfval  20775  marepvfval  20780  submafval  20794  submaval  20796  madufval  20852  minmar1fval  20861  mat2pmatfval  20939  cpm2mfval  20965  decpmatval0  20980  decpmatval  20981  pmatcollpw3lem  20999  xkoval  21803  xkopt  21871  xpstopnlem1  22025  submtmd  22320  blfvalps  22600  ishtpy  23183  isphtpy  23192  pcofval  23221  rrxip  23600  q1pval  24354  r1pval  24357  taylfval  24554  midf  26128  ismidb  26130  ttgval  26228  wwlksnon  27204  wspthsnon  27205  clwwlknonmpt2  27495  grpodivfval  27965  dipfval  28133  submatres  30474  lmatval  30481  lmatcl  30484  qqhval  30620  sxval  30855  sitmval  31013  cndprobval  31098  mclsval  32063  csbfinxpg  33823  rrnval  34255  ldualset  35284  paddfval  35956  tgrpfset  36903  tgrpset  36904  erngfset  36958  erngset  36959  erngfset-rN  36966  erngset-rN  36967  dvafset  37163  dvaset  37164  dvhfset  37239  dvhset  37240  djaffvalN  37292  djafvalN  37293  djhffval  37555  djhfval  37556  hlhilset  38093  eldiophb  38290  mendval  38722  hoidmvval  41728  ovnhoi  41754  hspval  41760  hspmbllem2  41778  hoimbl  41782  rngcvalALTV  42986  rngccoALTV  43013  funcrngcsetcALT  43024  ringcvalALTV  43032  ringccoALTV  43076  lincop  43222  lines  43477  rrxlines  43479  spheres  43492