Theorem opeq12d 4818

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Hypotheses

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
opeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
opeq12d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		opeq12 4812	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  nfopd  4827  moop2  5419  iunopeqop  5438  dfid2  5491  fsn2g  7005  funopsn  7015  fnprb  7079  fntpb  7080  fnpr2g  7081  fliftfuns  7179  dfmpo  7927  fsplit  7942  fsplitOLD  7943  fsplitfpar  7944  fnwelem  7957  fimaproj  7961  seqomlem0  8265  seqomlem1  8266  seqomlem4  8269  qliftfuns  8568  xpassen  8827  xpdom2  8828  xpf1o  8900  xpmapenlem  8905  xpmapen  8906  mapunen  8907  xpwdomg  9314  fseqenlem2  9774  nqereu  10678  addpipq2  10685  addpipq  10686  mulpipq2  10688  mulpipq  10689  1nqenq  10711  mulidnq  10712  ltexnq  10724  prlem934  10782  addsrmo  10822  mulsrmo  10823  addsrpr  10824  mulsrpr  10825  mulcnsr  10885  mulresr  10888  axcnre  10913  om2uzrdg  13666  uzrdgsuci  13670  pfxsuff1eqwrdeq  14402  swrdpfx  14410  ccatopth  14419  swrdccatin2d  14447  splval  14454  splcl  14455  cshfn  14493  repswcshw  14515  2swrd2eqwrdeq  14656  ruclem1  15930  eucalgval2  16276  qnumdenbi  16438  crth  16469  phimullem  16470  prmreclem3  16609  setsstruct  16867  ressval3d  16946  ressval3dOLD  16947  imasval  17212  imasaddvallem  17230  xpsff1o  17268  catidex  17373  cidval  17376  catcocl  17384  catass  17385  oppccofval  17416  sectfval  17453  subccocl  17550  isfunc  17569  funcco  17576  idfuval  17581  idfucl  17586  cofuval  17587  cofuval2  17592  cofucl  17593  cofuass  17594  cofulid  17595  cofurid  17596  resfval  17597  resfval2  17598  funcres  17601  isnat  17653  nati  17661  fucco  17670  fuccoval  17671  coaval  17773  catcisolem  17815  xpcval  17884  xpcco  17890  xpcco2  17894  xpccatid  17895  xpcid  17896  1stfval  17898  2ndfval  17901  1stfcl  17904  2ndfcl  17905  prfval  17906  prf1  17907  prf2fval  17908  prf2  17909  prfcl  17910  prf1st  17911  prf2nd  17912  1st2ndprf  17913  xpcpropd  17916  evlfval  17925  evlf2  17926  evlfcllem  17929  evlfcl  17930  curfval  17931  curf1  17933  curf1cl  17936  curf2cl  17939  curfcl  17940  curfpropd  17941  uncf1  17944  uncf2  17945  curfuncf  17946  uncfcurf  17947  diagval  17948  curf2ndf  17955  hofval  17960  hof2fval  17963  hofcl  17967  yonval  17969  hofpropd  17975  yonedalem21  17981  yonedalem22  17986  yonedalem3  17988  symg2bas  18990  mat1dimmul  21615  txcnp  22761  upxp  22764  uptx  22766  hauseqlcld  22787  txlm  22789  txkgen  22793  cnmpt1t  22806  cnmpt2t  22814  txhmeo  22944  flfcnp2  23148  ucnimalem  23422  ucnima  23423  fmucndlem  23433  fmucnd  23434  cnheiborlem  24107  pi1xfrcnvlem  24209  ovollb2lem  24642  ovollb2  24643  ovolshftlem2  24664  ovolscalem2  24668  ioombl1  24716  ioorf  24727  ioorval  24728  ioorinv2  24729  uniioombllem6  24742  dyadval  24746  opnmbl  24756  mbfimaopnlem  24809  limccnp2  25046  dvdsmulf1o  26333  ebtwntg  27340  numclwwlk1lem2fv  28708  numclwwlk1lem2fo  28710  numclwwlk1lem2  28712  wlkl0  28719  hhssnvt  29615  hhsssh  29619  opsbc2ie  30812  opreu2reuALT  30813  opfv  30970  xppreima  30971  2ndresdju  30974  aciunf1lem  30987  ofpreima  30990  fgreu  30997  smatlem  31735  qtophaus  31774  qqhval2  31920  esum2dlem  32048  rrvadd  32407  hgt750lemb  32624  bnj1442  33017  bnj1450  33018  bnj1463  33023  bnj1529  33038  swrdrevpfx  33066  erdszelem9  33149  erdszelem10  33150  txpconn  33182  txsconnlem  33190  goaleq12d  33301  msubval  33475  msubco  33481  mvhval  33484  msubvrs  33510  bj-dfid2ALT  35224  bj-endval  35474  finxpreclem3  35552  poimirlem4  35769  opnmbllem0  35801  mblfinlem1  35802  mblfinlem2  35803  heiborlem6  35962  heiborlem7  35963  heiborlem8  35964  nfopdALT  36973  dvhvaddcbv  39091  dvhvaddval  39092  dvhopvadd  39095  dvhvaddcomN  39098  dvhvaddass  39099  dvhvscacbv  39100  dvhvscaval  39101  dvhopvsca  39104  dvhgrp  39109  dvhlveclem  39110  dvh0g  39113  dvhopaddN  39116  dvhopspN  39117  dvhopN  39118  cdlemn4  39200  hdmapffval  39828  pellexlem3  40642  pellex  40646  elcnvlem  41171  dvnprodlem1  43450  dvnprodlem3  43452  etransclem44  43782  ovolval4  44152  ovolval5lem3  44155  aoveq123d  44630  prproropf1olem2  44917  prproropf1olem3  44918  prproropf1olem4  44919  prproropf1o  44920  prproropreud  44922  inclfusubc  45386  funcrngcsetc  45517  funcrngcsetcALT  45518  funcringcsetc  45554  mndtcval  46327  mndtcco  46333