Theorem mpoeq123dv 7525

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 7524	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  mpoeq123i  7526  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvv  8133  prdsval  17515  imasval  17571  imasvscaval  17598  homffval  17748  homfeq  17752  comfffval  17756  comffval  17757  comfffval2  17759  comffval2  17760  comfeq  17764  oppcval  17771  monfval  17793  sectffval  17811  invffval  17819  isofn  17836  cofuval  17946  natfval  18014  fucval  18027  fucco  18032  coafval  18131  setcval  18144  setcco  18150  catcval  18167  catcco  18172  estrcval  18192  estrcco  18198  xpcval  18246  1stfval  18260  2ndfval  18263  prfval  18268  evlfval  18287  evlf2  18288  curfval  18293  hofval  18322  hof2fval  18325  plusffval  18684  efmnd  18905  grpsubfval  19023  grpsubfvalALT  19024  grpsubpropd  19085  mulgfval  19109  mulgfvalALT  19110  mulgpropd  19156  lsmfval  19680  pj1fval  19736  efgtf  19764  prdsmgp  20178  dvrfval  20428  funcrngcsetcALT  20663  scaffval  20900  ipffval  21689  phssip  21699  frlmip  21821  psrval  21958  mamufval  22417  mvmulfval  22569  marrepfval  22587  marepvfval  22592  submafval  22606  submaval  22608  madufval  22664  minmar1fval  22673  mat2pmatfval  22750  cpm2mfval  22776  decpmatval0  22791  decpmatval  22792  pmatcollpw3lem  22810  xkoval  23616  xkopt  23684  xpstopnlem1  23838  submtmd  24133  blfvalps  24414  ishtpy  25023  isphtpy  25032  pcofval  25062  rrxip  25443  q1pval  26214  r1pval  26217  taylfval  26418  istrkgl  28484  midf  28802  ismidb  28804  ttgval  28901  ttgvalOLD  28902  wwlksnon  29884  wspthsnon  29885  clwwlknonmpo  30121  grpodivfval  30566  dipfval  30734  rlocval  33231  idlsrgval  33496  submatres  33752  lmatval  33759  lmatcl  33762  qqhval  33920  sxval  34154  sitmval  34314  cndprobval  34398  mclsval  35531  csbfinxpg  37354  rrnval  37787  ldualset  39081  paddfval  39754  tgrpfset  40701  tgrpset  40702  erngfset  40756  erngset  40757  erngfset-rN  40764  erngset-rN  40765  dvafset  40961  dvaset  40962  dvhfset  41037  dvhset  41038  djaffvalN  41090  djafvalN  41091  djhffval  41353  djhfval  41354  hlhilset  41891  eldiophb  42713  mendval  43140  mnringvald  44177  mnringmulrd  44190  hoidmvval  46498  ovnhoi  46524  hspval  46530  hspmbllem2  46548  hoimbl  46552  rngcvalALTV  47988  rngccoALTV  47994  ringcvalALTV  48012  ringccoALTV  48028  lincop  48137  lines  48465  rrxlines  48467  spheres  48480