Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpoeq123dv Structured version   Visualization version   GIF version

Theorem mpoeq123dv 7208
 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
StepHypRef Expression
1 mpoeq123dv.1 . 2 (𝜑𝐴 = 𝐷)
2 mpoeq123dv.2 . . 3 (𝜑𝐵 = 𝐸)
32adantr 484 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
4 mpoeq123dv.3 . . 3 (𝜑𝐶 = 𝐹)
54adantr 484 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
61, 3, 5mpoeq123dva 7207 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∈ cmpo 7137 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-oprab 7139  df-mpo 7140 This theorem is referenced by:  mpoeq123i  7209  mptmpoopabbrd  7763  el2mpocsbcl  7765  bropopvvv  7770  bropfvvvv  7772  prdsval  16722  imasval  16778  imasvscaval  16805  homffval  16954  homfeq  16958  comfffval  16962  comffval  16963  comfffval2  16965  comffval2  16966  comfeq  16970  oppcval  16977  monfval  16996  sectffval  17014  invffval  17022  isofn  17039  cofuval  17146  natfval  17210  fucval  17222  fucco  17226  coafval  17318  setcval  17331  setcco  17337  catcval  17350  catcco  17355  estrcval  17368  estrcco  17374  xpcval  17421  1stfval  17435  2ndfval  17438  prfval  17443  evlfval  17461  evlf2  17462  curfval  17467  hofval  17496  hof2fval  17499  plusffval  17852  efmnd  18029  grpsubfval  18142  grpsubfvalALT  18143  grpsubpropd  18199  mulgfval  18221  mulgfvalALT  18222  mulgpropd  18264  lsmfval  18758  pj1fval  18815  efgtf  18843  prdsmgp  19359  dvrfval  19433  scaffval  19648  ipffval  20341  phssip  20351  frlmip  20471  psrval  20604  mamufval  20999  mvmulfval  21154  marrepfval  21172  marepvfval  21177  submafval  21191  submaval  21193  madufval  21249  minmar1fval  21258  mat2pmatfval  21335  cpm2mfval  21361  decpmatval0  21376  decpmatval  21377  pmatcollpw3lem  21395  xkoval  22199  xkopt  22267  xpstopnlem1  22421  submtmd  22716  blfvalps  22997  ishtpy  23584  isphtpy  23593  pcofval  23622  rrxip  24001  q1pval  24761  r1pval  24764  taylfval  24961  midf  26577  ismidb  26579  ttgval  26676  wwlksnon  27644  wspthsnon  27645  clwwlknonmpo  27881  grpodivfval  28324  dipfval  28492  idlsrgval  31063  submatres  31171  lmatval  31178  lmatcl  31181  qqhval  31337  sxval  31571  sitmval  31729  cndprobval  31813  mclsval  32935  csbfinxpg  34821  rrnval  35281  ldualset  36437  paddfval  37109  tgrpfset  38056  tgrpset  38057  erngfset  38111  erngset  38112  erngfset-rN  38119  erngset-rN  38120  dvafset  38316  dvaset  38317  dvhfset  38392  dvhset  38393  djaffvalN  38445  djafvalN  38446  djhffval  38708  djhfval  38709  hlhilset  39246  eldiophb  39713  mendval  40142  mnringvald  40936  mnringmulrd  40946  hoidmvval  43231  ovnhoi  43257  hspval  43263  hspmbllem2  43281  hoimbl  43285  rngcvalALTV  44600  rngccoALTV  44627  funcrngcsetcALT  44638  ringcvalALTV  44646  ringccoALTV  44690  lincop  44831  lines  45159  rrxlines  45161  spheres  45174
 Copyright terms: Public domain W3C validator