Theorem opeq12d 4847

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  nfopd  4849  moop2  5473  iunopeqop  5493  iunopeqopOLD  5494  dfid2  5547  fsn2g  7139  funopsn  7151  funopsnOLD  7152  fnprb  7214  fntpb  7215  fnpr2g  7216  fliftfuns  7322  dfmpo  8115  fsplit  8130  fsplitfpar  8131  fnwelem  8145  fimaproj  8154  seqomlem0  8462  seqomlem1  8463  seqomlem4  8466  qliftfuns  8828  xpassen  9093  xpdom2  9094  xpf1o  9161  xpmapenlem  9166  xpmapen  9167  mapunen  9168  xpwdomg  9582  fseqenlem2  10107  nqereu  11017  addpipq2  11024  addpipq  11025  mulpipq2  11027  mulpipq  11028  1nqenq  11050  mulidnq  11051  ltexnq  11063  prlem934  11121  addsrmo  11161  mulsrmo  11162  addsrpr  11163  mulsrpr  11164  mulcnsr  11224  mulresr  11227  axcnre  11252  om2uzrdg  14102  uzrdgsuci  14106  pfxsuff1eqwrdeq  14852  swrdpfx  14860  ccatopth  14869  swrdccatin2d  14897  splval  14904  splcl  14905  swrdrevpfx  14922  cshfn  14945  repswcshw  14967  2swrd2eqwrdeq  15111  ruclem1  16404  eucalgval2  16761  qnumdenbi  16925  crth  16960  phimullem  16961  prmreclem3  17101  setsstruct  17359  ressval3d  17429  imasval  17688  imasaddvallem  17706  xpsff1o  17744  catidex  17853  cidval  17856  catcocl  17864  catass  17865  oppccofval  17895  sectfval  17931  subccocl  18025  isfunc  18044  funcco  18051  idfuval  18056  idfucl  18061  cofuval  18062  cofuval2  18067  cofucl  18068  cofuass  18069  cofulid  18070  cofurid  18071  resfval  18072  resfval2  18073  funcres  18076  inclfusubc  18123  isnat  18130  nati  18138  fucco  18145  fuccoval  18146  coaval  18248  catcisolem  18290  xpcval  18356  xpcco  18362  xpcco2  18366  xpccatid  18367  xpcid  18368  1stfval  18370  2ndfval  18373  1stfcl  18376  2ndfcl  18377  prfval  18378  prf1  18379  prf2fval  18380  prf2  18381  prfcl  18382  prf1st  18383  prf2nd  18384  1st2ndprf  18385  xpcpropd  18387  evlfval  18396  evlf2  18397  evlfcllem  18400  evlfcl  18401  curfval  18402  curf1  18404  curf1cl  18407  curf2cl  18410  curfcl  18411  curfpropd  18412  uncf1  18415  uncf2  18416  curfuncf  18417  uncfcurf  18418  diagval  18419  curf2ndf  18426  hofval  18431  hof2fval  18434  hofcl  18438  yonval  18440  hofpropd  18446  yonedalem21  18452  yonedalem22  18457  yonedalem3  18459  xpsmnd0  18977  xpsinv  19275  xpsgrpsub  19276  symg2bas  19612  xpsring1d  20568  funcrngcsetc  20897  funcrngcsetcALT  20898  funcringcsetc  20931  rngqiprngimfv  21599  rngqiprngghm  21600  rngqiprngimf1  21601  rngqiprngimfo  21602  rngqiprnglin  21603  rngqipring1  21617  rngqiprngfu  21618  pzriprnglem6  21797  pzriprnglem12  21803  mat1dimmul  22796  txcnp  23944  upxp  23947  uptx  23949  hauseqlcld  23970  txlm  23972  txkgen  23976  cnmpt1t  23989  cnmpt2t  23997  txhmeo  24127  flfcnp2  24331  ucnimalem  24603  ucnima  24604  fmucndlem  24614  fmucnd  24615  cnheiborlem  25280  pi1xfrcnvlem  25382  ovollb2lem  25814  ovollb2  25815  ovolshftlem2  25836  ovolscalem2  25840  ioombl1  25888  ioorf  25899  ioorval  25900  ioorinv2  25901  uniioombllem6  25914  dyadval  25918  opnmbl  25928  mbfimaopnlem  25981  limccnp2  26217  mpodvdsmulf1o  27526  dvdsmulf1o  27528  precsexlemcbv  28597  precsexlem3  28600  seqseq123d  28677  om2noseqrdg  28695  noseqrdgsuc  28699  ebtwntg  29565  numclwwlk1lem2fv  30962  numclwwlk1lem2fo  30964  numclwwlk1lem2  30966  wlkl0  30973  hhssnvt  31872  hhsssh  31876  opsbc2ie  33119  opreu2reuALT  33120  opfv  33285  xppreima  33286  2ndresdju  33290  aciunf1lem  33303  ofpreima  33306  fgreu  33312  gsumwrd2dccatlem  33684  gsumwrd2dccat  33685  rlocval  33866  rlocaddval  33876  rlocmulval  33877  rloccring  33878  rloc0g  33879  rloc1r  33880  rlocf1  33881  rlocinvunit  33882  rlocisunit  33883  zringfrac  34132  smatlem  34475  qtophaus  34514  qqhval2  34660  esum2dlem  34770  rrvadd  35130  hgt750lemb  35331  bnj1442  35725  bnj1450  35726  bnj1463  35731  bnj1529  35746  maxssj0  35945  erdszelem9  36050  erdszelem10  36051  txpconn  36083  txsconnlem  36091  goaleq12d  36202  msubval  36376  msubco  36382  mvhval  36385  msubvrs  36411  cbvoprab123vw  37120  cbvoprab23vw  37121  cbvoprab13vw  37122  cbvopabdavw  37147  cbvoprab123davw  37155  cbvoprab12davw  37156  cbvoprab23davw  37157  cbvoprab13davw  37158  bj-dfid2ALT  38072  bj-endval  38329  finxpreclem3  38409  poimirlem4  38635  opnmbllem0  38667  mblfinlem1  38668  mblfinlem2  38669  heiborlem6  38843  heiborlem7  38844  heiborlem8  38845  nfopdALT  40121  dvhvaddcbv  42239  dvhvaddval  42240  dvhopvadd  42243  dvhvaddcomN  42246  dvhvaddass  42247  dvhvscacbv  42248  dvhvscaval  42249  dvhopvsca  42252  dvhgrp  42257  dvhlveclem  42258  dvh0g  42261  dvhopaddN  42264  dvhopspN  42265  dvhopN  42266  cdlemn4  42348  hdmapffval  42976  pellexlem3  43931  pellex  43935  elcnvlem  44694  dvnprodlem1  47049  dvnprodlem3  47051  etransclem44  47381  ovolval4  47754  ovolval5lem3  47757  aoveq123d  48341  prproropf1olem2  48679  prproropf1olem3  48680  prproropf1olem4  48681  prproropf1o  48682  prproropreud  48684  isisubgr  49053  eloprab1st2nd  50072  ssccatid  50279  oppfvalg  50335  imaf1co  50364  uptrlem1  50419  xpcfucco3  50473  dfswapf2  50476  swapfval  50477  swapfcoa  50496  1stfpropd  50505  2ndfpropd  50506  tposcurf1  50514  diag1  50519  fuco2eld2  50529  fucofvalg  50533  fuco21  50551  fuco11bALT  50553  fuco23  50556  fuco22natlem3  50559  fuco22nat  50561  fucoid  50563  fuco22a  50565  fucocolem2  50569  fucocolem4  50571  postcofval  50589  precofval  50595  precofvalALT  50596  precofval3  50599  prcofvalg  50604  prcofpropd  50607  prcofdiag1  50621  prcofdiag  50622  fucoppcco  50637  oppfdiag1  50642  oppfdiag  50644  termcfuncval  50760  diag1f1olem  50761  termcfunc1eq  50763  mndtcval  50810  mndtcco  50816  2arwcatlem2  50827  2arwcatlem3  50828  2arwcatlem4  50829  2arwcat  50831  setc1onsubc  50833  parmapfunc2  50867  parmapfunc  50868  lanfval  50889  ranfval  50890  ranup  50918  concom  50939  islmd  50941