Theorem opeq12d 4410

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

Syntax hints:   → wi 4   = wceq 1483  ⟨cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  nfopd  4419  moop2  4966  iunopeqop  4981  fsn2g  6405  funopsn  6413  fnprb  6472  fntpb  6473  fnpr2g  6474  fliftfuns  6564  dfmpt2  7267  fsplit  7282  fnwelem  7292  seqomlem0  7544  seqomlem1  7545  seqomlem4  7548  qliftfuns  7834  xpassen  8054  xpdom2  8055  xpf1o  8122  xpmapenlem  8127  xpmapen  8128  mapunen  8129  xpwdomg  8490  fseqenlem2  8848  nqereu  9751  addpipq2  9758  addpipq  9759  mulpipq2  9761  mulpipq  9762  1nqenq  9784  mulidnq  9785  ltexnq  9797  prlem934  9855  addsrmo  9894  mulsrmo  9895  addsrpr  9896  mulsrpr  9897  mulcnsr  9957  mulresr  9960  axcnre  9985  om2uzrdg  12755  uzrdgsuci  12759  2swrd1eqwrdeq  13454  swrdswrd0  13462  ccatopth  13470  swrdccatin2d  13500  splval  13502  splcl  13503  cshfn  13536  repswcshw  13558  2swrd2eqwrdeq  13696  ruclem1  14960  eucalgval2  15294  qnumdenbi  15452  crth  15483  phimullem  15484  prmreclem3  15622  setsstruct  15898  ressval3d  15937  imasval  16171  imasaddvallem  16189  xpsff1o  16228  catidex  16335  cidval  16338  catcocl  16346  catass  16347  oppccofval  16376  sectfval  16411  subccocl  16505  isfunc  16524  funcco  16531  idfuval  16536  idfucl  16541  cofuval  16542  cofuval2  16547  cofucl  16548  cofuass  16549  cofulid  16550  cofurid  16551  resfval  16552  resfval2  16553  funcres  16556  isnat  16607  nati  16615  fucco  16622  fuccoval  16623  coaval  16718  catcisolem  16756  xpcval  16817  xpcco  16823  xpcco2  16827  xpccatid  16828  xpcid  16829  1stfval  16831  2ndfval  16834  1stfcl  16837  2ndfcl  16838  prfval  16839  prf1  16840  prf2fval  16841  prf2  16842  prfcl  16843  prf1st  16844  prf2nd  16845  1st2ndprf  16846  xpcpropd  16848  evlfval  16857  evlf2  16858  evlfcllem  16861  evlfcl  16862  curfval  16863  curf1  16865  curf1cl  16868  curf2cl  16871  curfcl  16872  curfpropd  16873  uncf1  16876  uncf2  16877  curfuncf  16878  uncfcurf  16879  diagval  16880  curf2ndf  16887  hofval  16892  hof2fval  16895  hofcl  16899  yonval  16901  hofpropd  16907  yonedalem21  16913  yonedalem22  16918  yonedalem3  16920  symg2bas  17818  mat1dimmul  20282  txcnp  21423  upxp  21426  uptx  21428  hauseqlcld  21449  txlm  21451  txkgen  21455  cnmpt1t  21468  cnmpt2t  21476  txhmeo  21606  flfcnp2  21811  ucnimalem  22084  ucnima  22085  fmucndlem  22095  fmucnd  22096  cnheiborlem  22753  pi1xfrcnvlem  22856  ovollb2lem  23256  ovollb2  23257  ovolshftlem2  23278  ovolscalem2  23282  ioombl1  23330  ioorf  23341  ioorval  23342  ioorinv2  23343  uniioombllem6  23356  dyadval  23360  opnmbl  23370  mbfimaopnlem  23422  limccnp2  23656  dvdsmulf1o  24920  ebtwntg  25862  numclwlk1lem2fv  27226  numclwlk1lem2fo  27228  numclwlk1lem2  27230  hhssnvt  28122  hhsssh  28126  opfv  29448  xppreima  29449  aciunf1lem  29462  ofpreima  29465  fgreu  29471  smatlem  29863  fimaproj  29900  qtophaus  29903  qqhval2  30026  esum2dlem  30154  rrvadd  30514  hgt750lemb  30734  bnj1442  31117  bnj1450  31118  bnj1463  31123  bnj1529  31138  erdszelem9  31181  erdszelem10  31182  txpconn  31214  txsconnlem  31222  msubval  31422  msubco  31428  mvhval  31431  msubvrs  31457  finxpreclem3  33230  poimirlem4  33413  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  heiborlem6  33615  heiborlem7  33616  heiborlem8  33617  nfopdALT  34258  dvhvaddcbv  36378  dvhvaddval  36379  dvhopvadd  36382  dvhvaddcomN  36385  dvhvaddass  36386  dvhvscacbv  36387  dvhvscaval  36388  dvhopvsca  36391  dvhgrp  36396  dvhlveclem  36397  dvh0g  36400  dvhopaddN  36403  dvhopspN  36404  dvhopN  36405  cdlemn4  36487  hdmapffval  37118  pellexlem3  37395  pellex  37399  elcnvlem  37907  dvnprodlem1  40161  dvnprodlem3  40163  etransclem44  40495  ovolval4  40865  ovolval5lem3  40868  aoveq123d  41258  pfxsuff1eqwrdeq  41407  inclfusubc  41867  funcrngcsetc  41998  funcrngcsetcALT  41999  funcringcsetc  42035