Theorem opeq12d 4817

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

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4571

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572

This theorem is referenced by:  nfopd  4826  moop2  5429  iunopeqop  5448  dfid2  5502  fsn2g  7042  funopsn  7052  fnprb  7116  fntpb  7117  fnpr2g  7118  fliftfuns  7217  dfmpo  7974  fsplit  7989  fsplitfpar  7990  fnwelem  8003  fimaproj  8007  seqomlem0  8311  seqomlem1  8312  seqomlem4  8315  qliftfuns  8624  xpassen  8891  xpdom2  8892  xpf1o  8964  xpmapenlem  8969  xpmapen  8970  mapunen  8971  xpwdomg  9388  fseqenlem2  9827  nqereu  10731  addpipq2  10738  addpipq  10739  mulpipq2  10741  mulpipq  10742  1nqenq  10764  mulidnq  10765  ltexnq  10777  prlem934  10835  addsrmo  10875  mulsrmo  10876  addsrpr  10877  mulsrpr  10878  mulcnsr  10938  mulresr  10941  axcnre  10966  om2uzrdg  13722  uzrdgsuci  13726  pfxsuff1eqwrdeq  14457  swrdpfx  14465  ccatopth  14474  swrdccatin2d  14502  splval  14509  splcl  14510  cshfn  14548  repswcshw  14570  2swrd2eqwrdeq  14711  ruclem1  15985  eucalgval2  16331  qnumdenbi  16493  crth  16524  phimullem  16525  prmreclem3  16664  setsstruct  16922  ressval3d  17001  ressval3dOLD  17002  imasval  17267  imasaddvallem  17285  xpsff1o  17323  catidex  17428  cidval  17431  catcocl  17439  catass  17440  oppccofval  17471  sectfval  17508  subccocl  17605  isfunc  17624  funcco  17631  idfuval  17636  idfucl  17641  cofuval  17642  cofuval2  17647  cofucl  17648  cofuass  17649  cofulid  17650  cofurid  17651  resfval  17652  resfval2  17653  funcres  17656  isnat  17708  nati  17716  fucco  17725  fuccoval  17726  coaval  17828  catcisolem  17870  xpcval  17939  xpcco  17945  xpcco2  17949  xpccatid  17950  xpcid  17951  1stfval  17953  2ndfval  17956  1stfcl  17959  2ndfcl  17960  prfval  17961  prf1  17962  prf2fval  17963  prf2  17964  prfcl  17965  prf1st  17966  prf2nd  17967  1st2ndprf  17968  xpcpropd  17971  evlfval  17980  evlf2  17981  evlfcllem  17984  evlfcl  17985  curfval  17986  curf1  17988  curf1cl  17991  curf2cl  17994  curfcl  17995  curfpropd  17996  uncf1  17999  uncf2  18000  curfuncf  18001  uncfcurf  18002  diagval  18003  curf2ndf  18010  hofval  18015  hof2fval  18018  hofcl  18022  yonval  18024  hofpropd  18030  yonedalem21  18036  yonedalem22  18041  yonedalem3  18043  symg2bas  19045  mat1dimmul  21670  txcnp  22816  upxp  22819  uptx  22821  hauseqlcld  22842  txlm  22844  txkgen  22848  cnmpt1t  22861  cnmpt2t  22869  txhmeo  22999  flfcnp2  23203  ucnimalem  23477  ucnima  23478  fmucndlem  23488  fmucnd  23489  cnheiborlem  24162  pi1xfrcnvlem  24264  ovollb2lem  24697  ovollb2  24698  ovolshftlem2  24719  ovolscalem2  24723  ioombl1  24771  ioorf  24782  ioorval  24783  ioorinv2  24784  uniioombllem6  24797  dyadval  24801  opnmbl  24811  mbfimaopnlem  24864  limccnp2  25101  dvdsmulf1o  26388  ebtwntg  27395  numclwwlk1lem2fv  28765  numclwwlk1lem2fo  28767  numclwwlk1lem2  28769  wlkl0  28776  hhssnvt  29672  hhsssh  29676  opsbc2ie  30869  opreu2reuALT  30870  opfv  31027  xppreima  31028  2ndresdju  31031  aciunf1lem  31044  ofpreima  31047  fgreu  31054  smatlem  31792  qtophaus  31831  qqhval2  31977  esum2dlem  32105  rrvadd  32464  hgt750lemb  32681  bnj1442  33074  bnj1450  33075  bnj1463  33080  bnj1529  33095  swrdrevpfx  33123  erdszelem9  33206  erdszelem10  33207  txpconn  33239  txsconnlem  33247  goaleq12d  33358  msubval  33532  msubco  33538  mvhval  33541  msubvrs  33567  bj-dfid2ALT  35280  bj-endval  35530  finxpreclem3  35608  poimirlem4  35825  opnmbllem0  35857  mblfinlem1  35858  mblfinlem2  35859  heiborlem6  36018  heiborlem7  36019  heiborlem8  36020  nfopdALT  37027  dvhvaddcbv  39145  dvhvaddval  39146  dvhopvadd  39149  dvhvaddcomN  39152  dvhvaddass  39153  dvhvscacbv  39154  dvhvscaval  39155  dvhopvsca  39158  dvhgrp  39163  dvhlveclem  39164  dvh0g  39167  dvhopaddN  39170  dvhopspN  39171  dvhopN  39172  cdlemn4  39254  hdmapffval  39882  pellexlem3  40690  pellex  40694  elcnvlem  41247  dvnprodlem1  43536  dvnprodlem3  43538  etransclem44  43868  ovolval4  44239  ovolval5lem3  44242  aoveq123d  44728  prproropf1olem2  45014  prproropf1olem3  45015  prproropf1olem4  45016  prproropf1o  45017  prproropreud  45019  inclfusubc  45483  funcrngcsetc  45614  funcrngcsetcALT  45615  funcringcsetc  45651  mndtcval  46424  mndtcco  46430