Theorem opeq12d 4842

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

Syntax hints:   → wi 4   = wceq 1563  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  nfopd  4851  moop2  5476  iunopeqop  5495  iunopeqopOLD  5496  dfid2  5549  fsn2g  7124  funopsn  7134  funopsnOLD  7135  fnprb  7196  fntpb  7197  fnpr2g  7198  fliftfuns  7302  dfmpo  8085  fsplit  8100  fsplitfpar  8101  fnwelem  8115  fimaproj  8119  seqomlem0  8424  seqomlem1  8425  seqomlem4  8428  qliftfuns  8790  xpassen  9047  xpdom2  9048  xpf1o  9115  xpmapenlem  9120  xpmapen  9121  mapunen  9122  xpwdomg  9535  fseqenlem2  9997  nqereu  10902  addpipq2  10909  addpipq  10910  mulpipq2  10912  mulpipq  10913  1nqenq  10935  mulidnq  10936  ltexnq  10948  prlem934  11006  addsrmo  11046  mulsrmo  11047  addsrpr  11048  mulsrpr  11049  mulcnsr  11109  mulresr  11112  axcnre  11137  om2uzrdg  13983  uzrdgsuci  13987  pfxsuff1eqwrdeq  14726  swrdpfx  14734  ccatopth  14743  swrdccatin2d  14771  splval  14778  splcl  14779  cshfn  14817  repswcshw  14839  2swrd2eqwrdeq  14980  ruclem1  16277  eucalgval2  16629  qnumdenbi  16793  crth  16827  phimullem  16828  prmreclem3  16968  setsstruct  17226  ressval3d  17296  imasval  17555  imasaddvallem  17573  xpsff1o  17611  catidex  17720  cidval  17723  catcocl  17731  catass  17732  oppccofval  17762  sectfval  17798  subccocl  17892  isfunc  17911  funcco  17918  idfuval  17923  idfucl  17928  cofuval  17929  cofuval2  17934  cofucl  17935  cofuass  17936  cofulid  17937  cofurid  17938  resfval  17939  resfval2  17940  funcres  17943  inclfusubc  17990  isnat  17997  nati  18005  fucco  18012  fuccoval  18013  coaval  18115  catcisolem  18157  xpcval  18223  xpcco  18229  xpcco2  18233  xpccatid  18234  xpcid  18235  1stfval  18237  2ndfval  18240  1stfcl  18243  2ndfcl  18244  prfval  18245  prf1  18246  prf2fval  18247  prf2  18248  prfcl  18249  prf1st  18250  prf2nd  18251  1st2ndprf  18252  xpcpropd  18254  evlfval  18263  evlf2  18264  evlfcllem  18267  evlfcl  18268  curfval  18269  curf1  18271  curf1cl  18274  curf2cl  18277  curfcl  18278  curfpropd  18279  uncf1  18282  uncf2  18283  curfuncf  18284  uncfcurf  18285  diagval  18286  curf2ndf  18293  hofval  18298  hof2fval  18301  hofcl  18305  yonval  18307  hofpropd  18313  yonedalem21  18319  yonedalem22  18324  yonedalem3  18326  xpsmnd0  18826  xpsinv  19117  xpsgrpsub  19118  symg2bas  19454  xpsring1d  20406  funcrngcsetc  20716  funcrngcsetcALT  20717  funcringcsetc  20750  rngqiprngimfv  21400  rngqiprngghm  21401  rngqiprngimf1  21402  rngqiprngimfo  21403  rngqiprnglin  21404  rngqipring1  21418  rngqiprngfu  21419  pzriprnglem6  21596  pzriprnglem12  21602  mat1dimmul  22594  txcnp  23738  upxp  23741  uptx  23743  hauseqlcld  23764  txlm  23766  txkgen  23770  cnmpt1t  23783  cnmpt2t  23791  txhmeo  23921  flfcnp2  24125  ucnimalem  24397  ucnima  24398  fmucndlem  24408  fmucnd  24409  cnheiborlem  25074  pi1xfrcnvlem  25176  ovollb2lem  25608  ovollb2  25609  ovolshftlem2  25630  ovolscalem2  25634  ioombl1  25682  ioorf  25693  ioorval  25694  ioorinv2  25695  uniioombllem6  25708  dyadval  25712  opnmbl  25722  mbfimaopnlem  25775  limccnp2  26012  mpodvdsmulf1o  27316  dvdsmulf1o  27318  precsexlemcbv  28357  precsexlem3  28360  seqseq123d  28437  om2noseqrdg  28455  noseqrdgsuc  28459  ebtwntg  29241  numclwwlk1lem2fv  30616  numclwwlk1lem2fo  30618  numclwwlk1lem2  30620  wlkl0  30627  hhssnvt  31526  hhsssh  31530  opsbc2ie  32732  opreu2reuALT  32733  opfv  32901  xppreima  32902  2ndresdju  32906  aciunf1lem  32919  ofpreima  32922  fgreu  32928  gsumwrd2dccatlem  33310  gsumwrd2dccat  33311  rlocval  33492  rlocaddval  33502  rlocmulval  33503  rloccring  33504  rloc0g  33505  rloc1r  33506  rlocf1  33507  rlocinvunit  33508  rlocisunit  33509  zringfrac  33761  smatlem  34104  qtophaus  34143  qqhval2  34289  esum2dlem  34399  rrvadd  34759  hgt750lemb  34960  bnj1442  35354  bnj1450  35355  bnj1463  35360  bnj1529  35375  swrdrevpfx  35479  erdszelem9  35562  erdszelem10  35563  txpconn  35595  txsconnlem  35603  goaleq12d  35714  msubval  35888  msubco  35894  mvhval  35897  msubvrs  35923  cbvoprab123vw  36612  cbvoprab23vw  36613  cbvoprab13vw  36614  cbvopabdavw  36639  cbvoprab123davw  36647  cbvoprab12davw  36648  cbvoprab23davw  36649  cbvoprab13davw  36650  bj-dfid2ALT  37562  bj-endval  37819  finxpreclem3  37899  poimirlem4  38135  opnmbllem0  38167  mblfinlem1  38168  mblfinlem2  38169  heiborlem6  38327  heiborlem7  38328  heiborlem8  38329  nfopdALT  39607  dvhvaddcbv  41725  dvhvaddval  41726  dvhopvadd  41729  dvhvaddcomN  41732  dvhvaddass  41733  dvhvscacbv  41734  dvhvscaval  41735  dvhopvsca  41738  dvhgrp  41743  dvhlveclem  41744  dvh0g  41747  dvhopaddN  41750  dvhopspN  41751  dvhopN  41752  cdlemn4  41834  hdmapffval  42462  pellexlem3  43420  pellex  43424  elcnvlem  44189  dvnprodlem1  46518  dvnprodlem3  46520  etransclem44  46850  ovolval4  47223  ovolval5lem3  47226  aoveq123d  47770  prproropf1olem2  48108  prproropf1olem3  48109  prproropf1olem4  48110  prproropf1o  48111  prproropreud  48113  isisubgr  48482  eloprab1st2nd  49497  ssccatid  49701  oppfvalg  49755  imaf1co  49784  uptrlem1  49839  xpcfucco3  49887  dfswapf2  49890  swapfval  49891  swapfcoa  49910  1stfpropd  49919  2ndfpropd  49920  tposcurf1  49928  diag1  49933  fuco2eld2  49943  fucofvalg  49947  fuco21  49965  fuco11bALT  49967  fuco23  49970  fuco22natlem3  49973  fuco22nat  49975  fucoid  49977  fuco22a  49979  fucocolem2  49983  fucocolem4  49985  postcofval  49993  precofval  49996  precofvalALT  49997  precofval3  50000  prcofvalg  50005  prcofpropd  50008  prcofdiag1  50022  prcofdiag  50023  fucoppcco  50038  oppfdiag1  50043  oppfdiag  50045  termcfuncval  50161  diag1f1olem  50162  mndtcval  50208  mndtcco  50214  2arwcatlem2  50225  2arwcatlem3  50226  2arwcatlem4  50227  2arwcat  50229  setc1onsubc  50231  lanfval  50242  ranfval  50243  ranup  50271  concom  50292  islmd  50294