Theorem mpoeq123dv 7229

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ∈ cmpo 7158

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  mpoeq123i  7230  mptmpoopabbrd  7778  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvv  7787  prdsval  16728  imasval  16784  imasvscaval  16811  homffval  16960  homfeq  16964  comfffval  16968  comffval  16969  comfffval2  16971  comffval2  16972  comfeq  16976  oppcval  16983  monfval  17002  sectffval  17020  invffval  17028  isofn  17045  cofuval  17152  natfval  17216  fucval  17228  fucco  17232  coafval  17324  setcval  17337  setcco  17343  catcval  17356  catcco  17361  estrcval  17374  estrcco  17380  xpcval  17427  1stfval  17441  2ndfval  17444  prfval  17449  evlfval  17467  evlf2  17468  curfval  17473  hofval  17502  hof2fval  17505  plusffval  17858  efmnd  18035  grpsubfval  18147  grpsubfvalALT  18148  grpsubpropd  18204  mulgfval  18226  mulgfvalALT  18227  mulgpropd  18269  lsmfval  18763  pj1fval  18820  efgtf  18848  prdsmgp  19360  dvrfval  19434  scaffval  19652  psrval  20142  ipffval  20792  phssip  20802  frlmip  20922  mamufval  20996  mvmulfval  21151  marrepfval  21169  marepvfval  21174  submafval  21188  submaval  21190  madufval  21246  minmar1fval  21255  mat2pmatfval  21331  cpm2mfval  21357  decpmatval0  21372  decpmatval  21373  pmatcollpw3lem  21391  xkoval  22195  xkopt  22263  xpstopnlem1  22417  submtmd  22712  blfvalps  22993  ishtpy  23576  isphtpy  23585  pcofval  23614  rrxip  23993  q1pval  24747  r1pval  24750  taylfval  24947  midf  26562  ismidb  26564  ttgval  26661  wwlksnon  27629  wspthsnon  27630  clwwlknonmpo  27868  grpodivfval  28311  dipfval  28479  submatres  31071  lmatval  31078  lmatcl  31081  qqhval  31215  sxval  31449  sitmval  31607  cndprobval  31691  mclsval  32810  csbfinxpg  34672  rrnval  35120  ldualset  36276  paddfval  36948  tgrpfset  37895  tgrpset  37896  erngfset  37950  erngset  37951  erngfset-rN  37958  erngset-rN  37959  dvafset  38155  dvaset  38156  dvhfset  38231  dvhset  38232  djaffvalN  38284  djafvalN  38285  djhffval  38547  djhfval  38548  hlhilset  39085  eldiophb  39374  mendval  39803  hoidmvval  42879  ovnhoi  42905  hspval  42911  hspmbllem2  42929  hoimbl  42933  rngcvalALTV  44252  rngccoALTV  44279  funcrngcsetcALT  44290  ringcvalALTV  44298  ringccoALTV  44342  lincop  44483  lines  44738  rrxlines  44740  spheres  44753