Theorem opeq12d 4881

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  nfopd  4890  moop2  5507  iunopeqop  5526  dfid2  5580  fsn2g  7158  funopsn  7168  fnprb  7228  fntpb  7229  fnpr2g  7230  fliftfuns  7334  dfmpo  8127  fsplit  8142  fsplitfpar  8143  fnwelem  8156  fimaproj  8160  seqomlem0  8489  seqomlem1  8490  seqomlem4  8493  qliftfuns  8844  xpassen  9106  xpdom2  9107  xpf1o  9179  xpmapenlem  9184  xpmapen  9185  mapunen  9186  xpwdomg  9625  fseqenlem2  10065  nqereu  10969  addpipq2  10976  addpipq  10977  mulpipq2  10979  mulpipq  10980  1nqenq  11002  mulidnq  11003  ltexnq  11015  prlem934  11073  addsrmo  11113  mulsrmo  11114  addsrpr  11115  mulsrpr  11116  mulcnsr  11176  mulresr  11179  axcnre  11204  om2uzrdg  13997  uzrdgsuci  14001  pfxsuff1eqwrdeq  14737  swrdpfx  14745  ccatopth  14754  swrdccatin2d  14782  splval  14789  splcl  14790  cshfn  14828  repswcshw  14850  2swrd2eqwrdeq  14992  ruclem1  16267  eucalgval2  16618  qnumdenbi  16781  crth  16815  phimullem  16816  prmreclem3  16956  setsstruct  17213  ressval3d  17292  imasval  17556  imasaddvallem  17574  xpsff1o  17612  catidex  17717  cidval  17720  catcocl  17728  catass  17729  oppccofval  17759  sectfval  17795  subccocl  17890  isfunc  17909  funcco  17916  idfuval  17921  idfucl  17926  cofuval  17927  cofuval2  17932  cofucl  17933  cofuass  17934  cofulid  17935  cofurid  17936  resfval  17937  resfval2  17938  funcres  17941  inclfusubc  17988  isnat  17995  nati  18003  fucco  18010  fuccoval  18011  coaval  18113  catcisolem  18155  xpcval  18222  xpcco  18228  xpcco2  18232  xpccatid  18233  xpcid  18234  1stfval  18236  2ndfval  18239  1stfcl  18242  2ndfcl  18243  prfval  18244  prf1  18245  prf2fval  18246  prf2  18247  prfcl  18248  prf1st  18249  prf2nd  18250  1st2ndprf  18251  xpcpropd  18253  evlfval  18262  evlf2  18263  evlfcllem  18266  evlfcl  18267  curfval  18268  curf1  18270  curf1cl  18273  curf2cl  18276  curfcl  18277  curfpropd  18278  uncf1  18281  uncf2  18282  curfuncf  18283  uncfcurf  18284  diagval  18285  curf2ndf  18292  hofval  18297  hof2fval  18300  hofcl  18304  yonval  18306  hofpropd  18312  yonedalem21  18318  yonedalem22  18323  yonedalem3  18325  xpsmnd0  18791  xpsinv  19078  xpsgrpsub  19079  symg2bas  19410  xpsring1d  20330  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  rngqiprngimfv  21308  rngqiprngghm  21309  rngqiprngimf1  21310  rngqiprngimfo  21311  rngqiprnglin  21312  rngqipring1  21326  rngqiprngfu  21327  pzriprnglem6  21497  pzriprnglem12  21503  mat1dimmul  22482  txcnp  23628  upxp  23631  uptx  23633  hauseqlcld  23654  txlm  23656  txkgen  23660  cnmpt1t  23673  cnmpt2t  23681  txhmeo  23811  flfcnp2  24015  ucnimalem  24289  ucnima  24290  fmucndlem  24300  fmucnd  24301  cnheiborlem  24986  pi1xfrcnvlem  25089  ovollb2lem  25523  ovollb2  25524  ovolshftlem2  25545  ovolscalem2  25549  ioombl1  25597  ioorf  25608  ioorval  25609  ioorinv2  25610  uniioombllem6  25623  dyadval  25627  opnmbl  25637  mbfimaopnlem  25690  limccnp2  25927  mpodvdsmulf1o  27237  dvdsmulf1o  27239  precsexlemcbv  28230  precsexlem3  28233  seqseq123d  28292  om2noseqrdg  28310  noseqrdgsuc  28314  ebtwntg  28997  numclwwlk1lem2fv  30375  numclwwlk1lem2fo  30377  numclwwlk1lem2  30379  wlkl0  30386  hhssnvt  31284  hhsssh  31288  opsbc2ie  32495  opreu2reuALT  32496  opfv  32654  xppreima  32655  2ndresdju  32659  aciunf1lem  32672  ofpreima  32675  fgreu  32682  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  rlocval  33263  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  zringfrac  33582  smatlem  33796  qtophaus  33835  qqhval2  33983  esum2dlem  34093  rrvadd  34454  hgt750lemb  34671  bnj1442  35063  bnj1450  35064  bnj1463  35069  bnj1529  35084  swrdrevpfx  35122  erdszelem9  35204  erdszelem10  35205  txpconn  35237  txsconnlem  35245  goaleq12d  35356  msubval  35530  msubco  35536  mvhval  35539  msubvrs  35565  cbvoprab123vw  36240  cbvoprab23vw  36241  cbvoprab13vw  36242  cbvopabdavw  36267  cbvoprab123davw  36275  cbvoprab12davw  36276  cbvoprab23davw  36277  cbvoprab13davw  36278  bj-dfid2ALT  37066  bj-endval  37316  finxpreclem3  37394  poimirlem4  37631  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  nfopdALT  38972  dvhvaddcbv  41091  dvhvaddval  41092  dvhopvadd  41095  dvhvaddcomN  41098  dvhvaddass  41099  dvhvscacbv  41100  dvhvscaval  41101  dvhopvsca  41104  dvhgrp  41109  dvhlveclem  41110  dvh0g  41113  dvhopaddN  41116  dvhopspN  41117  dvhopN  41118  cdlemn4  41200  hdmapffval  41828  pellexlem3  42842  pellex  42846  elcnvlem  43614  dvnprodlem1  45961  dvnprodlem3  45963  etransclem44  46293  ovolval4  46666  ovolval5lem3  46669  aoveq123d  47190  prproropf1olem2  47491  prproropf1olem3  47492  prproropf1olem4  47493  prproropf1o  47494  prproropreud  47496  isisubgr  47848  xpcfucco3  48964  dfswapf2  48967  swapfval  48968  swapfcoa  48987  tposcurf1  48999  diag1  49004  fuco2eld2  49009  fucofvalg  49013  fuco21  49031  fuco11bALT  49033  fuco23  49036  fuco22natlem3  49039  fuco22nat  49041  fucoid  49043  fuco22a  49045  fucocolem2  49049  fucocolem4  49051  postcofval  49059  precofval  49062  precofvalALT  49063  precoffunc  49066  mndtcval  49176  mndtcco  49182