Theorem opeq12d 4840

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

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

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 4584  df-pr 4586  df-op 4590

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  8113  fsplit  8128  fsplitfpar  8129  fnwelem  8143  fimaproj  8152  seqomlem0  8459  seqomlem1  8460  seqomlem4  8463  qliftfuns  8825  xpassen  9090  xpdom2  9091  xpf1o  9158  xpmapenlem  9163  xpmapen  9164  mapunen  9165  xpwdomg  9579  fseqenlem2  10104  nqereu  11014  addpipq2  11021  addpipq  11022  mulpipq2  11024  mulpipq  11025  1nqenq  11047  mulidnq  11048  ltexnq  11060  prlem934  11118  addsrmo  11158  mulsrmo  11159  addsrpr  11160  mulsrpr  11161  mulcnsr  11221  mulresr  11224  axcnre  11249  om2uzrdg  14099  uzrdgsuci  14103  pfxsuff1eqwrdeq  14848  swrdpfx  14856  ccatopth  14865  swrdccatin2d  14893  splval  14900  splcl  14901  swrdrevpfx  14918  cshfn  14941  repswcshw  14963  2swrd2eqwrdeq  15106  ruclem1  16399  eucalgval2  16756  qnumdenbi  16920  crth  16955  phimullem  16956  prmreclem3  17096  setsstruct  17354  ressval3d  17424  imasval  17683  imasaddvallem  17701  xpsff1o  17739  catidex  17848  cidval  17851  catcocl  17859  catass  17860  oppccofval  17890  sectfval  17926  subccocl  18020  isfunc  18039  funcco  18046  idfuval  18051  idfucl  18056  cofuval  18057  cofuval2  18062  cofucl  18063  cofuass  18064  cofulid  18065  cofurid  18066  resfval  18067  resfval2  18068  funcres  18071  inclfusubc  18118  isnat  18125  nati  18133  fucco  18140  fuccoval  18141  coaval  18243  catcisolem  18285  xpcval  18351  xpcco  18357  xpcco2  18361  xpccatid  18362  xpcid  18363  1stfval  18365  2ndfval  18368  1stfcl  18371  2ndfcl  18372  prfval  18373  prf1  18374  prf2fval  18375  prf2  18376  prfcl  18377  prf1st  18378  prf2nd  18379  1st2ndprf  18380  xpcpropd  18382  evlfval  18391  evlf2  18392  evlfcllem  18395  evlfcl  18396  curfval  18397  curf1  18399  curf1cl  18402  curf2cl  18405  curfcl  18406  curfpropd  18407  uncf1  18410  uncf2  18411  curfuncf  18412  uncfcurf  18413  diagval  18414  curf2ndf  18421  hofval  18426  hof2fval  18429  hofcl  18433  yonval  18435  hofpropd  18441  yonedalem21  18447  yonedalem22  18452  yonedalem3  18454  xpsmnd0  18972  xpsinv  19270  xpsgrpsub  19271  symg2bas  19607  xpsring1d  20563  funcrngcsetc  20892  funcrngcsetcALT  20893  funcringcsetc  20926  rngqiprngimfv  21594  rngqiprngghm  21595  rngqiprngimf1  21596  rngqiprngimfo  21597  rngqiprnglin  21598  rngqipring1  21612  rngqiprngfu  21613  pzriprnglem6  21792  pzriprnglem12  21798  mat1dimmul  22791  txcnp  23939  upxp  23942  uptx  23944  hauseqlcld  23965  txlm  23967  txkgen  23971  cnmpt1t  23984  cnmpt2t  23992  txhmeo  24122  flfcnp2  24326  ucnimalem  24598  ucnima  24599  fmucndlem  24609  fmucnd  24610  cnheiborlem  25275  pi1xfrcnvlem  25377  ovollb2lem  25809  ovollb2  25810  ovolshftlem2  25831  ovolscalem2  25835  ioombl1  25883  ioorf  25894  ioorval  25895  ioorinv2  25896  uniioombllem6  25909  dyadval  25913  opnmbl  25923  mbfimaopnlem  25976  limccnp2  26212  mpodvdsmulf1o  27521  dvdsmulf1o  27523  precsexlemcbv  28592  precsexlem3  28595  seqseq123d  28672  om2noseqrdg  28690  noseqrdgsuc  28694  ebtwntg  29560  numclwwlk1lem2fv  30957  numclwwlk1lem2fo  30959  numclwwlk1lem2  30961  wlkl0  30968  hhssnvt  31867  hhsssh  31871  opsbc2ie  33072  opreu2reuALT  33073  opfv  33238  xppreima  33239  2ndresdju  33243  aciunf1lem  33256  ofpreima  33259  fgreu  33265  gsumwrd2dccatlem  33638  gsumwrd2dccat  33639  rlocval  33820  rlocaddval  33830  rlocmulval  33831  rloccring  33832  rloc0g  33833  rloc1r  33834  rlocf1  33835  rlocinvunit  33836  rlocisunit  33837  zringfrac  34086  smatlem  34429  qtophaus  34468  qqhval2  34614  esum2dlem  34724  rrvadd  35084  hgt750lemb  35285  bnj1442  35679  bnj1450  35680  bnj1463  35685  bnj1529  35700  erdszelem9  35964  erdszelem10  35965  txpconn  35997  txsconnlem  36005  goaleq12d  36116  msubval  36290  msubco  36296  mvhval  36299  msubvrs  36325  cbvoprab123vw  37028  cbvoprab23vw  37029  cbvoprab13vw  37030  cbvopabdavw  37055  cbvoprab123davw  37063  cbvoprab12davw  37064  cbvoprab23davw  37065  cbvoprab13davw  37066  bj-dfid2ALT  37980  bj-endval  38237  finxpreclem3  38317  poimirlem4  38543  opnmbllem0  38575  mblfinlem1  38576  mblfinlem2  38577  heiborlem6  38751  heiborlem7  38752  heiborlem8  38753  nfopdALT  40029  dvhvaddcbv  42147  dvhvaddval  42148  dvhopvadd  42151  dvhvaddcomN  42154  dvhvaddass  42155  dvhvscacbv  42156  dvhvscaval  42157  dvhopvsca  42160  dvhgrp  42165  dvhlveclem  42166  dvh0g  42169  dvhopaddN  42172  dvhopspN  42173  dvhopN  42174  cdlemn4  42256  hdmapffval  42884  pellexlem3  43838  pellex  43842  elcnvlem  44601  dvnprodlem1  46956  dvnprodlem3  46958  etransclem44  47288  ovolval4  47661  ovolval5lem3  47664  aoveq123d  48248  prproropf1olem2  48586  prproropf1olem3  48587  prproropf1olem4  48588  prproropf1o  48589  prproropreud  48591  isisubgr  48960  eloprab1st2nd  49978  ssccatid  50180  oppfvalg  50234  imaf1co  50263  uptrlem1  50318  xpcfucco3  50366  dfswapf2  50369  swapfval  50370  swapfcoa  50389  1stfpropd  50398  2ndfpropd  50399  tposcurf1  50407  diag1  50412  fuco2eld2  50422  fucofvalg  50426  fuco21  50444  fuco11bALT  50446  fuco23  50449  fuco22natlem3  50452  fuco22nat  50454  fucoid  50456  fuco22a  50458  fucocolem2  50462  fucocolem4  50464  postcofval  50472  precofval  50475  precofvalALT  50476  precofval3  50479  prcofvalg  50484  prcofpropd  50487  prcofdiag1  50501  prcofdiag  50502  fucoppcco  50517  oppfdiag1  50522  oppfdiag  50524  termcfuncval  50640  diag1f1olem  50641  mndtcval  50687  mndtcco  50693  2arwcatlem2  50704  2arwcatlem3  50705  2arwcatlem4  50706  2arwcat  50708  setc1onsubc  50710  lanfval  50721  ranfval  50722  ranup  50750  concom  50771  islmd  50773