Theorem mpoeq123dv 7430

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

Hypotheses

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem mpoeq123dv

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
2		mpoeq123dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐸)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
4		mpoeq123dv.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐹)
5	4	adantr 480	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
6	1, 3, 5	mpoeq123dva 7429	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∈ cmpo 7357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-oprab 7359  df-mpo 7360

This theorem is referenced by:  mpoeq123i  7431  mptmpoopabbrd  8021  mptmpoopabbrdOLD  8022  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvv  8031  prdsval  17366  imasval  17423  imasvscaval  17450  homffval  17604  homfeq  17608  comfffval  17612  comffval  17613  comfffval2  17615  comffval2  17616  comfeq  17620  oppcval  17627  monfval  17647  sectffval  17665  invffval  17673  isofn  17690  cofuval  17797  natfval  17864  fucval  17876  fucco  17880  coafval  17979  setcval  17992  setcco  17998  catcval  18015  catcco  18020  estrcval  18038  estrcco  18044  xpcval  18091  1stfval  18105  2ndfval  18108  prfval  18113  evlfval  18131  evlf2  18132  curfval  18137  hofval  18166  hof2fval  18169  plusffval  18562  efmnd  18786  grpsubfval  18904  grpsubfvalALT  18905  grpsubpropd  18966  mulgfval  18990  mulgfvalALT  18991  mulgpropd  19037  lsmfval  19558  pj1fval  19614  efgtf  19642  prdsmgp  20077  dvrfval  20329  funcrngcsetcALT  20565  scaffval  20822  ipffval  21594  phssip  21604  frlmip  21724  psrval  21862  mamufval  22327  mvmulfval  22477  marrepfval  22495  marepvfval  22500  submafval  22514  submaval  22516  madufval  22572  minmar1fval  22581  mat2pmatfval  22658  cpm2mfval  22684  decpmatval0  22699  decpmatval  22700  pmatcollpw3lem  22718  xkoval  23522  xkopt  23590  xpstopnlem1  23744  submtmd  24039  blfvalps  24318  ishtpy  24918  isphtpy  24927  pcofval  24957  rrxip  25337  q1pval  26107  r1pval  26110  taylfval  26313  istrkgl  28456  midf  28774  ismidb  28776  ttgval  28873  wwlksnon  29850  wspthsnon  29851  clwwlknonmpo  30090  grpodivfval  30535  dipfval  30703  rlocval  33269  idlsrgval  33512  splyval  33645  submatres  33891  lmatval  33898  lmatcl  33901  qqhval  34057  sxval  34275  sitmval  34434  cndprobval  34518  mclsval  35679  csbfinxpg  37505  rrnval  37940  ldualset  39297  paddfval  39969  tgrpfset  40916  tgrpset  40917  erngfset  40971  erngset  40972  erngfset-rN  40979  erngset-rN  40980  dvafset  41176  dvaset  41177  dvhfset  41252  dvhset  41253  djaffvalN  41305  djafvalN  41306  djhffval  41568  djhfval  41569  hlhilset  42106  eldiophb  42914  mendval  43336  mnringvald  44370  mnringmulrd  44380  hoidmvval  46737  ovnhoi  46763  hspval  46769  hspmbllem2  46787  hoimbl  46791  rngcvalALTV  48427  rngccoALTV  48433  ringcvalALTV  48451  ringccoALTV  48467  lincop  48570  lines  48893  rrxlines  48895  spheres  48908  invfn  49191  infsubc2  49222  imaidfu2  49272  upfval  49337  dfswapf2  49422  swapfval  49423  1stfpropd  49451  2ndfpropd  49452  fucofvalg  49479  fuco21  49497  precofval3  49532  prcofvalg  49537  setc1ocofval  49655  lanfval  49774  ranfval  49775