Theorem opeq12d 4880

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

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

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634

This theorem is referenced by:  nfopd  4889  moop2  5501  iunopeqop  5520  dfid2  5575  fsn2g  7137  funopsn  7147  fnprb  7211  fntpb  7212  fnpr2g  7213  fliftfuns  7313  dfmpo  8090  fsplit  8105  fsplitfpar  8106  fnwelem  8119  fimaproj  8123  seqomlem0  8451  seqomlem1  8452  seqomlem4  8455  qliftfuns  8800  xpassen  9068  xpdom2  9069  xpf1o  9141  xpmapenlem  9146  xpmapen  9147  mapunen  9148  xpwdomg  9582  fseqenlem2  10022  nqereu  10926  addpipq2  10933  addpipq  10934  mulpipq2  10936  mulpipq  10937  1nqenq  10959  mulidnq  10960  ltexnq  10972  prlem934  11030  addsrmo  11070  mulsrmo  11071  addsrpr  11072  mulsrpr  11073  mulcnsr  11133  mulresr  11136  axcnre  11161  om2uzrdg  13925  uzrdgsuci  13929  pfxsuff1eqwrdeq  14653  swrdpfx  14661  ccatopth  14670  swrdccatin2d  14698  splval  14705  splcl  14706  cshfn  14744  repswcshw  14766  2swrd2eqwrdeq  14908  ruclem1  16178  eucalgval2  16522  qnumdenbi  16684  crth  16715  phimullem  16716  prmreclem3  16855  setsstruct  17113  ressval3d  17195  ressval3dOLD  17196  imasval  17461  imasaddvallem  17479  xpsff1o  17517  catidex  17622  cidval  17625  catcocl  17633  catass  17634  oppccofval  17665  sectfval  17702  subccocl  17799  isfunc  17818  funcco  17825  idfuval  17830  idfucl  17835  cofuval  17836  cofuval2  17841  cofucl  17842  cofuass  17843  cofulid  17844  cofurid  17845  resfval  17846  resfval2  17847  funcres  17850  isnat  17902  nati  17910  fucco  17919  fuccoval  17920  coaval  18022  catcisolem  18064  xpcval  18133  xpcco  18139  xpcco2  18143  xpccatid  18144  xpcid  18145  1stfval  18147  2ndfval  18150  1stfcl  18153  2ndfcl  18154  prfval  18155  prf1  18156  prf2fval  18157  prf2  18158  prfcl  18159  prf1st  18160  prf2nd  18161  1st2ndprf  18162  xpcpropd  18165  evlfval  18174  evlf2  18175  evlfcllem  18178  evlfcl  18179  curfval  18180  curf1  18182  curf1cl  18185  curf2cl  18188  curfcl  18189  curfpropd  18190  uncf1  18193  uncf2  18194  curfuncf  18195  uncfcurf  18196  diagval  18197  curf2ndf  18204  hofval  18209  hof2fval  18212  hofcl  18216  yonval  18218  hofpropd  18224  yonedalem21  18230  yonedalem22  18235  yonedalem3  18237  xpsmnd0  18700  xpsinv  18979  xpsgrpsub  18980  symg2bas  19301  xpsring1d  20221  rngqiprngimfv  21057  rngqiprngghm  21058  rngqiprngimf1  21059  rngqiprngimfo  21060  rngqiprnglin  21061  rngqipring1  21075  rngqiprngfu  21076  pzriprnglem6  21255  pzriprnglem12  21261  mat1dimmul  22198  txcnp  23344  upxp  23347  uptx  23349  hauseqlcld  23370  txlm  23372  txkgen  23376  cnmpt1t  23389  cnmpt2t  23397  txhmeo  23527  flfcnp2  23731  ucnimalem  24005  ucnima  24006  fmucndlem  24016  fmucnd  24017  cnheiborlem  24700  pi1xfrcnvlem  24803  ovollb2lem  25237  ovollb2  25238  ovolshftlem2  25259  ovolscalem2  25263  ioombl1  25311  ioorf  25322  ioorval  25323  ioorinv2  25324  uniioombllem6  25337  dyadval  25341  opnmbl  25351  mbfimaopnlem  25404  limccnp2  25641  dvdsmulf1o  26934  precsexlemcbv  27891  precsexlem3  27894  ebtwntg  28507  numclwwlk1lem2fv  29876  numclwwlk1lem2fo  29878  numclwwlk1lem2  29880  wlkl0  29887  hhssnvt  30785  hhsssh  30789  opsbc2ie  31983  opreu2reuALT  31984  opfv  32137  xppreima  32138  2ndresdju  32141  aciunf1lem  32154  ofpreima  32157  fgreu  32164  smatlem  33075  qtophaus  33114  qqhval2  33260  esum2dlem  33388  rrvadd  33749  hgt750lemb  33966  bnj1442  34358  bnj1450  34359  bnj1463  34364  bnj1529  34379  swrdrevpfx  34405  erdszelem9  34488  erdszelem10  34489  txpconn  34521  txsconnlem  34529  goaleq12d  34640  msubval  34814  msubco  34820  mvhval  34823  msubvrs  34849  bj-dfid2ALT  36249  bj-endval  36499  finxpreclem3  36577  poimirlem4  36795  opnmbllem0  36827  mblfinlem1  36828  mblfinlem2  36829  heiborlem6  36987  heiborlem7  36988  heiborlem8  36989  nfopdALT  38144  dvhvaddcbv  40263  dvhvaddval  40264  dvhopvadd  40267  dvhvaddcomN  40270  dvhvaddass  40271  dvhvscacbv  40272  dvhvscaval  40273  dvhopvsca  40276  dvhgrp  40281  dvhlveclem  40282  dvh0g  40285  dvhopaddN  40288  dvhopspN  40289  dvhopN  40290  cdlemn4  40372  hdmapffval  41000  pellexlem3  41871  pellex  41875  elcnvlem  42654  dvnprodlem1  44960  dvnprodlem3  44962  etransclem44  45292  ovolval4  45665  ovolval5lem3  45668  aoveq123d  46184  prproropf1olem2  46470  prproropf1olem3  46471  prproropf1olem4  46472  prproropf1o  46473  prproropreud  46475  inclfusubc  46907  funcrngcsetc  46984  funcrngcsetcALT  46985  funcringcsetc  47021  mndtcval  47792  mndtcco  47798