Theorem mpt2eq123dv 6884

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2140   ↦ cmpt2 6817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-oprab 6819  df-mpt2 6820

This theorem is referenced by:  mpt2eq123i  6885  mptmpt2opabbrd  7418  el2mpt2csbcl  7420  bropopvvv  7425  bropfvvvv  7427  prdsval  16338  imasval  16394  imasvscaval  16421  homffval  16572  homfeq  16576  comfffval  16580  comffval  16581  comfffval2  16583  comffval2  16584  comfeq  16588  oppcval  16595  monfval  16614  sectffval  16632  invffval  16640  isofn  16657  cofuval  16764  natfval  16828  fucval  16840  fucco  16844  coafval  16936  setcval  16949  setcco  16955  catcval  16968  catcco  16973  estrcval  16986  estrcco  16992  xpcval  17039  xpchomfval  17041  xpccofval  17044  1stfval  17053  2ndfval  17056  prfval  17061  evlfval  17079  evlf2  17080  curfval  17085  hofval  17114  hof2fval  17117  plusffval  17469  grpsubfval  17686  grpsubpropd  17742  mulgfval  17764  mulgpropd  17806  symgval  18020  lsmfval  18274  pj1fval  18328  efgtf  18356  prdsmgp  18831  dvrfval  18905  scaffval  19104  psrval  19585  ipffval  20216  phssip  20226  frlmip  20340  mamufval  20414  mvmulfval  20571  marrepfval  20589  marepvfval  20594  submafval  20608  submaval  20610  madufval  20666  minmar1fval  20675  mat2pmatfval  20751  cpm2mfval  20777  decpmatval0  20792  decpmatval  20793  pmatcollpw3lem  20811  xkoval  21613  xkopt  21681  xpstopnlem1  21835  submtmd  22130  blfvalps  22410  ishtpy  22993  isphtpy  23002  pcofval  23031  rrxip  23399  q1pval  24133  r1pval  24136  taylfval  24333  midf  25889  ismidb  25891  ttgval  25976  wwlksnon  26977  wspthsnon  26978  clwwlknonmpt2  27256  grpodivfval  27719  dipfval  27888  submatres  30203  lmatval  30210  lmatcl  30213  qqhval  30349  sxval  30584  sitmval  30742  cndprobval  30826  mclsval  31789  csbfinxpg  33555  rrnval  33958  ldualset  34934  paddfval  35605  tgrpfset  36553  tgrpset  36554  erngfset  36608  erngset  36609  erngfset-rN  36616  erngset-rN  36617  dvafset  36813  dvaset  36814  dvhfset  36890  dvhset  36891  djaffvalN  36943  djafvalN  36944  djhffval  37206  djhfval  37207  hlhilset  37747  eldiophb  37841  mendval  38274  hoidmvval  41316  ovnhoi  41342  hspval  41348  hspmbllem2  41366  hoimbl  41370  rngcvalALTV  42490  rngccoALTV  42517  funcrngcsetcALT  42528  ringcvalALTV  42536  ringccoALTV  42580  lincop  42726