Theorem opeq12d 4885

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

Syntax hints:   → wi 4   = wceq 1536  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  nfopd  4894  moop2  5511  iunopeqop  5530  dfid2  5584  fsn2g  7157  funopsn  7167  fnprb  7227  fntpb  7228  fnpr2g  7229  fliftfuns  7333  dfmpo  8125  fsplit  8140  fsplitfpar  8141  fnwelem  8154  fimaproj  8158  seqomlem0  8487  seqomlem1  8488  seqomlem4  8491  qliftfuns  8842  xpassen  9104  xpdom2  9105  xpf1o  9177  xpmapenlem  9182  xpmapen  9183  mapunen  9184  xpwdomg  9622  fseqenlem2  10062  nqereu  10966  addpipq2  10973  addpipq  10974  mulpipq2  10976  mulpipq  10977  1nqenq  10999  mulidnq  11000  ltexnq  11012  prlem934  11070  addsrmo  11110  mulsrmo  11111  addsrpr  11112  mulsrpr  11113  mulcnsr  11173  mulresr  11176  axcnre  11201  om2uzrdg  13993  uzrdgsuci  13997  pfxsuff1eqwrdeq  14733  swrdpfx  14741  ccatopth  14750  swrdccatin2d  14778  splval  14785  splcl  14786  cshfn  14824  repswcshw  14846  2swrd2eqwrdeq  14988  ruclem1  16263  eucalgval2  16614  qnumdenbi  16777  crth  16811  phimullem  16812  prmreclem3  16951  setsstruct  17209  ressval3d  17291  ressval3dOLD  17292  imasval  17557  imasaddvallem  17575  xpsff1o  17613  catidex  17718  cidval  17721  catcocl  17729  catass  17730  oppccofval  17761  sectfval  17798  subccocl  17895  isfunc  17914  funcco  17921  idfuval  17926  idfucl  17931  cofuval  17932  cofuval2  17937  cofucl  17938  cofuass  17939  cofulid  17940  cofurid  17941  resfval  17942  resfval2  17943  funcres  17946  inclfusubc  17994  isnat  18001  nati  18009  fucco  18018  fuccoval  18019  coaval  18121  catcisolem  18163  xpcval  18232  xpcco  18238  xpcco2  18242  xpccatid  18243  xpcid  18244  1stfval  18246  2ndfval  18249  1stfcl  18252  2ndfcl  18253  prfval  18254  prf1  18255  prf2fval  18256  prf2  18257  prfcl  18258  prf1st  18259  prf2nd  18260  1st2ndprf  18261  xpcpropd  18264  evlfval  18273  evlf2  18274  evlfcllem  18277  evlfcl  18278  curfval  18279  curf1  18281  curf1cl  18284  curf2cl  18287  curfcl  18288  curfpropd  18289  uncf1  18292  uncf2  18293  curfuncf  18294  uncfcurf  18295  diagval  18296  curf2ndf  18303  hofval  18308  hof2fval  18311  hofcl  18315  yonval  18317  hofpropd  18323  yonedalem21  18329  yonedalem22  18334  yonedalem3  18336  xpsmnd0  18803  xpsinv  19090  xpsgrpsub  19091  symg2bas  19424  xpsring1d  20346  funcrngcsetc  20656  funcrngcsetcALT  20657  funcringcsetc  20690  rngqiprngimfv  21325  rngqiprngghm  21326  rngqiprngimf1  21327  rngqiprngimfo  21328  rngqiprnglin  21329  rngqipring1  21343  rngqiprngfu  21344  pzriprnglem6  21514  pzriprnglem12  21520  mat1dimmul  22497  txcnp  23643  upxp  23646  uptx  23648  hauseqlcld  23669  txlm  23671  txkgen  23675  cnmpt1t  23688  cnmpt2t  23696  txhmeo  23826  flfcnp2  24030  ucnimalem  24304  ucnima  24305  fmucndlem  24315  fmucnd  24316  cnheiborlem  24999  pi1xfrcnvlem  25102  ovollb2lem  25536  ovollb2  25537  ovolshftlem2  25558  ovolscalem2  25562  ioombl1  25610  ioorf  25621  ioorval  25622  ioorinv2  25623  uniioombllem6  25636  dyadval  25640  opnmbl  25650  mbfimaopnlem  25703  limccnp2  25941  mpodvdsmulf1o  27251  dvdsmulf1o  27253  precsexlemcbv  28244  precsexlem3  28247  seqseq123d  28306  om2noseqrdg  28324  noseqrdgsuc  28328  ebtwntg  29011  numclwwlk1lem2fv  30384  numclwwlk1lem2fo  30386  numclwwlk1lem2  30388  wlkl0  30395  hhssnvt  31293  hhsssh  31297  opsbc2ie  32503  opreu2reuALT  32504  opfv  32660  xppreima  32661  2ndresdju  32665  aciunf1lem  32678  ofpreima  32681  fgreu  32688  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  rlocval  33245  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rloc0g  33257  rloc1r  33258  rlocf1  33259  zringfrac  33561  smatlem  33757  qtophaus  33796  qqhval2  33944  esum2dlem  34072  rrvadd  34433  hgt750lemb  34649  bnj1442  35041  bnj1450  35042  bnj1463  35047  bnj1529  35062  swrdrevpfx  35100  erdszelem9  35183  erdszelem10  35184  txpconn  35216  txsconnlem  35224  goaleq12d  35335  msubval  35509  msubco  35515  mvhval  35518  msubvrs  35544  cbvoprab123vw  36221  cbvoprab23vw  36222  cbvoprab13vw  36223  cbvopabdavw  36248  cbvoprab123davw  36256  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  bj-dfid2ALT  37047  bj-endval  37297  finxpreclem3  37375  poimirlem4  37610  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  nfopdALT  38952  dvhvaddcbv  41071  dvhvaddval  41072  dvhopvadd  41075  dvhvaddcomN  41078  dvhvaddass  41079  dvhvscacbv  41080  dvhvscaval  41081  dvhopvsca  41084  dvhgrp  41089  dvhlveclem  41090  dvh0g  41093  dvhopaddN  41096  dvhopspN  41097  dvhopN  41098  cdlemn4  41180  hdmapffval  41808  pellexlem3  42818  pellex  42822  elcnvlem  43590  dvnprodlem1  45901  dvnprodlem3  45903  etransclem44  46233  ovolval4  46606  ovolval5lem3  46609  aoveq123d  47127  prproropf1olem2  47428  prproropf1olem3  47429  prproropf1olem4  47430  prproropf1o  47431  prproropreud  47433  isisubgr  47785  mndtcval  48887  mndtcco  48893