Theorem opeq12d 4845

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 4839	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  nfopd  4854  moop2  5462  iunopeqop  5481  dfid2  5535  fsn2g  7110  funopsn  7120  fnprb  7182  fntpb  7183  fnpr2g  7184  fliftfuns  7289  dfmpo  8081  fsplit  8096  fsplitfpar  8097  fnwelem  8110  fimaproj  8114  seqomlem0  8417  seqomlem1  8418  seqomlem4  8421  qliftfuns  8777  xpassen  9035  xpdom2  9036  xpf1o  9103  xpmapenlem  9108  xpmapen  9109  mapunen  9110  xpwdomg  9538  fseqenlem2  9978  nqereu  10882  addpipq2  10889  addpipq  10890  mulpipq2  10892  mulpipq  10893  1nqenq  10915  mulidnq  10916  ltexnq  10928  prlem934  10986  addsrmo  11026  mulsrmo  11027  addsrpr  11028  mulsrpr  11029  mulcnsr  11089  mulresr  11092  axcnre  11117  om2uzrdg  13921  uzrdgsuci  13925  pfxsuff1eqwrdeq  14664  swrdpfx  14672  ccatopth  14681  swrdccatin2d  14709  splval  14716  splcl  14717  cshfn  14755  repswcshw  14777  2swrd2eqwrdeq  14919  ruclem1  16199  eucalgval2  16551  qnumdenbi  16714  crth  16748  phimullem  16749  prmreclem3  16889  setsstruct  17146  ressval3d  17216  imasval  17474  imasaddvallem  17492  xpsff1o  17530  catidex  17635  cidval  17638  catcocl  17646  catass  17647  oppccofval  17677  sectfval  17713  subccocl  17807  isfunc  17826  funcco  17833  idfuval  17838  idfucl  17843  cofuval  17844  cofuval2  17849  cofucl  17850  cofuass  17851  cofulid  17852  cofurid  17853  resfval  17854  resfval2  17855  funcres  17858  inclfusubc  17905  isnat  17912  nati  17920  fucco  17927  fuccoval  17928  coaval  18030  catcisolem  18072  xpcval  18138  xpcco  18144  xpcco2  18148  xpccatid  18149  xpcid  18150  1stfval  18152  2ndfval  18155  1stfcl  18158  2ndfcl  18159  prfval  18160  prf1  18161  prf2fval  18162  prf2  18163  prfcl  18164  prf1st  18165  prf2nd  18166  1st2ndprf  18167  xpcpropd  18169  evlfval  18178  evlf2  18179  evlfcllem  18182  evlfcl  18183  curfval  18184  curf1  18186  curf1cl  18189  curf2cl  18192  curfcl  18193  curfpropd  18194  uncf1  18197  uncf2  18198  curfuncf  18199  uncfcurf  18200  diagval  18201  curf2ndf  18208  hofval  18213  hof2fval  18216  hofcl  18220  yonval  18222  hofpropd  18228  yonedalem21  18234  yonedalem22  18239  yonedalem3  18241  xpsmnd0  18705  xpsinv  18992  xpsgrpsub  18993  symg2bas  19323  xpsring1d  20242  funcrngcsetc  20549  funcrngcsetcALT  20550  funcringcsetc  20583  rngqiprngimfv  21208  rngqiprngghm  21209  rngqiprngimf1  21210  rngqiprngimfo  21211  rngqiprnglin  21212  rngqipring1  21226  rngqiprngfu  21227  pzriprnglem6  21396  pzriprnglem12  21402  mat1dimmul  22363  txcnp  23507  upxp  23510  uptx  23512  hauseqlcld  23533  txlm  23535  txkgen  23539  cnmpt1t  23552  cnmpt2t  23560  txhmeo  23690  flfcnp2  23894  ucnimalem  24167  ucnima  24168  fmucndlem  24178  fmucnd  24179  cnheiborlem  24853  pi1xfrcnvlem  24956  ovollb2lem  25389  ovollb2  25390  ovolshftlem2  25411  ovolscalem2  25415  ioombl1  25463  ioorf  25474  ioorval  25475  ioorinv2  25476  uniioombllem6  25489  dyadval  25493  opnmbl  25503  mbfimaopnlem  25556  limccnp2  25793  mpodvdsmulf1o  27104  dvdsmulf1o  27106  precsexlemcbv  28108  precsexlem3  28111  seqseq123d  28180  om2noseqrdg  28198  noseqrdgsuc  28202  ebtwntg  28909  numclwwlk1lem2fv  30285  numclwwlk1lem2fo  30287  numclwwlk1lem2  30289  wlkl0  30296  hhssnvt  31194  hhsssh  31198  opsbc2ie  32405  opreu2reuALT  32406  opfv  32568  xppreima  32569  2ndresdju  32573  aciunf1lem  32586  ofpreima  32589  fgreu  32596  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  rlocval  33210  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rloc0g  33222  rloc1r  33223  rlocf1  33224  zringfrac  33525  smatlem  33787  qtophaus  33826  qqhval2  33972  esum2dlem  34082  rrvadd  34443  hgt750lemb  34647  bnj1442  35039  bnj1450  35040  bnj1463  35045  bnj1529  35060  swrdrevpfx  35104  erdszelem9  35186  erdszelem10  35187  txpconn  35219  txsconnlem  35227  goaleq12d  35338  msubval  35512  msubco  35518  mvhval  35521  msubvrs  35547  cbvoprab123vw  36227  cbvoprab23vw  36228  cbvoprab13vw  36229  cbvopabdavw  36254  cbvoprab123davw  36262  cbvoprab12davw  36263  cbvoprab23davw  36264  cbvoprab13davw  36265  bj-dfid2ALT  37053  bj-endval  37303  finxpreclem3  37381  poimirlem4  37618  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  nfopdALT  38964  dvhvaddcbv  41083  dvhvaddval  41084  dvhopvadd  41087  dvhvaddcomN  41090  dvhvaddass  41091  dvhvscacbv  41092  dvhvscaval  41093  dvhopvsca  41096  dvhgrp  41101  dvhlveclem  41102  dvh0g  41105  dvhopaddN  41108  dvhopspN  41109  dvhopN  41110  cdlemn4  41192  hdmapffval  41820  pellexlem3  42819  pellex  42823  elcnvlem  43590  dvnprodlem1  45944  dvnprodlem3  45946  etransclem44  46276  ovolval4  46649  ovolval5lem3  46652  aoveq123d  47179  prproropf1olem2  47505  prproropf1olem3  47506  prproropf1olem4  47507  prproropf1o  47508  prproropreud  47510  isisubgr  47862  eloprab1st2nd  48856  ssccatid  49061  oppfvalg  49115  imaf1co  49144  uptrlem1  49199  xpcfucco3  49247  dfswapf2  49250  swapfval  49251  swapfcoa  49270  1stfpropd  49279  2ndfpropd  49280  tposcurf1  49288  diag1  49293  fuco2eld2  49303  fucofvalg  49307  fuco21  49325  fuco11bALT  49327  fuco23  49330  fuco22natlem3  49333  fuco22nat  49335  fucoid  49337  fuco22a  49339  fucocolem2  49343  fucocolem4  49345  postcofval  49353  precofval  49356  precofvalALT  49357  precofval3  49360  prcofvalg  49365  prcofpropd  49368  prcofdiag1  49382  prcofdiag  49383  fucoppcco  49398  oppfdiag1  49403  oppfdiag  49405  termcfuncval  49521  diag1f1olem  49522  mndtcval  49568  mndtcco  49574  2arwcatlem2  49585  2arwcatlem3  49586  2arwcatlem4  49587  2arwcat  49589  setc1onsubc  49591  lanfval  49602  ranfval  49603  ranup  49631  concom  49652  islmd  49654