Theorem opeq12d 4813

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576

This theorem is referenced by:  nfopd  4822  moop2  5394  iunopeqop  5413  fsn2g  6902  funopsn  6912  fnprb  6973  fntpb  6974  fnpr2g  6975  fliftfuns  7069  dfmpo  7799  fsplit  7814  fsplitOLD  7815  fsplitfpar  7816  fnwelem  7827  fimaproj  7831  seqomlem0  8087  seqomlem1  8088  seqomlem4  8091  qliftfuns  8386  xpassen  8613  xpdom2  8614  xpf1o  8681  xpmapenlem  8686  xpmapen  8687  mapunen  8688  xpwdomg  9051  fseqenlem2  9453  nqereu  10353  addpipq2  10360  addpipq  10361  mulpipq2  10363  mulpipq  10364  1nqenq  10386  mulidnq  10387  ltexnq  10399  prlem934  10457  addsrmo  10497  mulsrmo  10498  addsrpr  10499  mulsrpr  10500  mulcnsr  10560  mulresr  10563  axcnre  10588  om2uzrdg  13327  uzrdgsuci  13331  pfxsuff1eqwrdeq  14063  swrdpfx  14071  ccatopth  14080  swrdccatin2d  14108  splval  14115  splcl  14116  cshfn  14154  repswcshw  14176  2swrd2eqwrdeq  14317  ruclem1  15586  eucalgval2  15927  qnumdenbi  16086  crth  16117  phimullem  16118  prmreclem3  16256  setsstruct  16525  ressval3d  16563  imasval  16786  imasaddvallem  16804  xpsff1o  16842  catidex  16947  cidval  16950  catcocl  16958  catass  16959  oppccofval  16988  sectfval  17023  subccocl  17117  isfunc  17136  funcco  17143  idfuval  17148  idfucl  17153  cofuval  17154  cofuval2  17159  cofucl  17160  cofuass  17161  cofulid  17162  cofurid  17163  resfval  17164  resfval2  17165  funcres  17168  isnat  17219  nati  17227  fucco  17234  fuccoval  17235  coaval  17330  catcisolem  17368  xpcval  17429  xpcco  17435  xpcco2  17439  xpccatid  17440  xpcid  17441  1stfval  17443  2ndfval  17446  1stfcl  17449  2ndfcl  17450  prfval  17451  prf1  17452  prf2fval  17453  prf2  17454  prfcl  17455  prf1st  17456  prf2nd  17457  1st2ndprf  17458  xpcpropd  17460  evlfval  17469  evlf2  17470  evlfcllem  17473  evlfcl  17474  curfval  17475  curf1  17477  curf1cl  17480  curf2cl  17483  curfcl  17484  curfpropd  17485  uncf1  17488  uncf2  17489  curfuncf  17490  uncfcurf  17491  diagval  17492  curf2ndf  17499  hofval  17504  hof2fval  17507  hofcl  17511  yonval  17513  hofpropd  17519  yonedalem21  17525  yonedalem22  17530  yonedalem3  17532  symg2bas  18523  mat1dimmul  21087  txcnp  22230  upxp  22233  uptx  22235  hauseqlcld  22256  txlm  22258  txkgen  22262  cnmpt1t  22275  cnmpt2t  22283  txhmeo  22413  flfcnp2  22617  ucnimalem  22891  ucnima  22892  fmucndlem  22902  fmucnd  22903  cnheiborlem  23560  pi1xfrcnvlem  23662  ovollb2lem  24091  ovollb2  24092  ovolshftlem2  24113  ovolscalem2  24117  ioombl1  24165  ioorf  24176  ioorval  24177  ioorinv2  24178  uniioombllem6  24191  dyadval  24195  opnmbl  24205  mbfimaopnlem  24258  limccnp2  24492  dvdsmulf1o  25773  ebtwntg  26770  numclwwlk1lem2fv  28137  numclwwlk1lem2fo  28139  numclwwlk1lem2  28141  wlkl0  28148  hhssnvt  29044  hhsssh  29048  opsbc2ie  30241  opreu2reuALT  30242  opfv  30395  xppreima  30396  aciunf1lem  30409  ofpreima  30412  fgreu  30419  smatlem  31064  qtophaus  31102  qqhval2  31225  esum2dlem  31353  rrvadd  31712  hgt750lemb  31929  bnj1442  32323  bnj1450  32324  bnj1463  32329  bnj1529  32344  swrdrevpfx  32365  erdszelem9  32448  erdszelem10  32449  txpconn  32481  txsconnlem  32489  goaleq12d  32600  msubval  32774  msubco  32780  mvhval  32783  msubvrs  32809  bj-endval  34598  finxpreclem3  34676  poimirlem4  34898  opnmbllem0  34930  mblfinlem1  34931  mblfinlem2  34932  heiborlem6  35096  heiborlem7  35097  heiborlem8  35098  nfopdALT  36109  dvhvaddcbv  38227  dvhvaddval  38228  dvhopvadd  38231  dvhvaddcomN  38234  dvhvaddass  38235  dvhvscacbv  38236  dvhvscaval  38237  dvhopvsca  38240  dvhgrp  38245  dvhlveclem  38246  dvh0g  38249  dvhopaddN  38252  dvhopspN  38253  dvhopN  38254  cdlemn4  38336  hdmapffval  38964  pellexlem3  39435  pellex  39439  elcnvlem  39968  dvnprodlem1  42238  dvnprodlem3  42240  etransclem44  42570  ovolval4  42940  ovolval5lem3  42943  aoveq123d  43384  prproropf1olem2  43673  prproropf1olem3  43674  prproropf1olem4  43675  prproropf1o  43676  prproropreud  43678  inclfusubc  44145  funcrngcsetc  44276  funcrngcsetcALT  44277  funcringcsetc  44313