Theorem mpt2eq123dv 6865

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145   ↦ cmpt2 6796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-oprab 6798  df-mpt2 6799

This theorem is referenced by:  mpt2eq123i  6866  mptmpt2opabbrd  7399  el2mpt2csbcl  7401  bropopvvv  7407  bropfvvvv  7409  prdsval  16324  imasval  16380  imasvscaval  16407  homffval  16558  homfeq  16562  comfffval  16566  comffval  16567  comfffval2  16569  comffval2  16570  comfeq  16574  oppcval  16581  monfval  16600  sectffval  16618  invffval  16626  isofn  16643  cofuval  16750  natfval  16814  fucval  16826  fucco  16830  coafval  16922  setcval  16935  setcco  16941  catcval  16954  catcco  16959  estrcval  16972  estrcco  16978  xpcval  17026  xpchomfval  17028  xpccofval  17031  1stfval  17040  2ndfval  17043  prfval  17048  evlfval  17066  evlf2  17067  curfval  17072  hofval  17101  hof2fval  17104  plusffval  17456  grpsubfval  17673  grpsubpropd  17729  mulgfval  17751  mulgpropd  17793  symgval  18007  lsmfval  18261  pj1fval  18315  efgtf  18343  prdsmgp  18819  dvrfval  18893  scaffval  19092  psrval  19578  ipffval  20211  phssip  20221  frlmip  20335  mamufval  20409  mvmulfval  20567  marrepfval  20585  marepvfval  20590  submafval  20604  submaval  20606  madufval  20662  minmar1fval  20671  mat2pmatfval  20749  cpm2mfval  20775  decpmatval0  20790  decpmatval  20791  pmatcollpw3lem  20809  xkoval  21612  xkopt  21680  xpstopnlem1  21834  submtmd  22129  blfvalps  22409  ishtpy  22992  isphtpy  23001  pcofval  23030  rrxip  23398  q1pval  24134  r1pval  24137  taylfval  24334  midf  25890  ismidb  25892  ttgval  25977  wwlksnon  26981  wspthsnon  26982  clwwlknonmpt2  27262  grpodivfval  27729  dipfval  27898  submatres  30213  lmatval  30220  lmatcl  30223  qqhval  30359  sxval  30594  sitmval  30752  cndprobval  30836  mclsval  31799  csbfinxpg  33563  rrnval  33959  ldualset  34935  paddfval  35606  tgrpfset  36554  tgrpset  36555  erngfset  36609  erngset  36610  erngfset-rN  36617  erngset-rN  36618  dvafset  36814  dvaset  36815  dvhfset  36891  dvhset  36892  djaffvalN  36944  djafvalN  36945  djhffval  37207  djhfval  37208  hlhilset  37745  eldiophb  37847  mendval  38280  hoidmvval  41312  ovnhoi  41338  hspval  41344  hspmbllem2  41362  hoimbl  41366  rngcvalALTV  42490  rngccoALTV  42517  funcrngcsetcALT  42528  ringcvalALTV  42536  ringccoALTV  42580  lincop  42726