Theorem mpoeq123dv 7486

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  mpoeq123i  7487  mptmpoopabbrd  8069  mptmpoopabbrdOLD  8071  el2mpocsbcl  8073  bropopvvv  8078  bropfvvvv  8080  prdsval  17403  imasval  17459  imasvscaval  17486  homffval  17636  homfeq  17640  comfffval  17644  comffval  17645  comfffval2  17647  comffval2  17648  comfeq  17652  oppcval  17659  monfval  17681  sectffval  17699  invffval  17707  isofn  17724  cofuval  17834  natfval  17899  fucval  17912  fucco  17917  coafval  18016  setcval  18029  setcco  18035  catcval  18052  catcco  18057  estrcval  18077  estrcco  18083  xpcval  18131  1stfval  18145  2ndfval  18148  prfval  18153  evlfval  18172  evlf2  18173  curfval  18178  hofval  18207  hof2fval  18210  plusffval  18569  efmnd  18753  grpsubfval  18870  grpsubfvalALT  18871  grpsubpropd  18930  mulgfval  18954  mulgfvalALT  18955  mulgpropd  18998  lsmfval  19508  pj1fval  19564  efgtf  19592  prdsmgp  20136  dvrfval  20220  scaffval  20495  ipffval  21207  phssip  21217  frlmip  21339  psrval  21474  mamufval  21894  mvmulfval  22051  marrepfval  22069  marepvfval  22074  submafval  22088  submaval  22090  madufval  22146  minmar1fval  22155  mat2pmatfval  22232  cpm2mfval  22258  decpmatval0  22273  decpmatval  22274  pmatcollpw3lem  22292  xkoval  23098  xkopt  23166  xpstopnlem1  23320  submtmd  23615  blfvalps  23896  ishtpy  24495  isphtpy  24504  pcofval  24533  rrxip  24914  q1pval  25678  r1pval  25681  taylfval  25878  istrkgl  27747  midf  28065  ismidb  28067  ttgval  28164  ttgvalOLD  28165  wwlksnon  29143  wspthsnon  29144  clwwlknonmpo  29380  grpodivfval  29825  dipfval  29993  idlsrgval  32662  submatres  32855  lmatval  32862  lmatcl  32865  qqhval  33023  sxval  33257  sitmval  33417  cndprobval  33501  mclsval  34623  csbfinxpg  36361  rrnval  36787  ldualset  38087  paddfval  38760  tgrpfset  39707  tgrpset  39708  erngfset  39762  erngset  39763  erngfset-rN  39770  erngset-rN  39771  dvafset  39967  dvaset  39968  dvhfset  40043  dvhset  40044  djaffvalN  40096  djafvalN  40097  djhffval  40359  djhfval  40360  hlhilset  40897  eldiophb  41583  mendval  42013  mnringvald  43055  mnringmulrd  43068  hoidmvval  45378  ovnhoi  45404  hspval  45410  hspmbllem2  45428  hoimbl  45432  rngcvalALTV  46944  rngccoALTV  46971  funcrngcsetcALT  46982  ringcvalALTV  46990  ringccoALTV  47034  lincop  47173  lines  47501  rrxlines  47503  spheres  47516