Theorem opeq12d 4844

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594

This theorem is used by:  nfopd  4853  moop2  5483  iunopeqop  5502  iunopeqopOLD  5503  dfid2  5556  fsn2g  7136  funopsn  7148  funopsnOLD  7149  fnprb  7211  fntpb  7212  fnpr2g  7213  fliftfuns  7319  dfmpo  8103  fsplit  8118  fsplitfpar  8119  fnwelem  8133  fimaproj  8137  seqomlem0  8442  seqomlem1  8443  seqomlem4  8446  qliftfuns  8808  xpassen  9073  xpdom2  9074  xpf1o  9141  xpmapenlem  9146  xpmapen  9147  mapunen  9148  xpwdomg  9561  fseqenlem2  10032  nqereu  10942  addpipq2  10949  addpipq  10950  mulpipq2  10952  mulpipq  10953  1nqenq  10975  mulidnq  10976  ltexnq  10988  prlem934  11046  addsrmo  11086  mulsrmo  11087  addsrpr  11088  mulsrpr  11089  mulcnsr  11149  mulresr  11152  axcnre  11177  om2uzrdg  14024  uzrdgsuci  14028  pfxsuff1eqwrdeq  14772  swrdpfx  14780  ccatopth  14789  swrdccatin2d  14817  splval  14824  splcl  14825  swrdrevpfx  14842  cshfn  14865  repswcshw  14887  2swrd2eqwrdeq  15030  ruclem1  16325  eucalgval2  16677  qnumdenbi  16841  crth  16875  phimullem  16876  prmreclem3  17016  setsstruct  17274  ressval3d  17344  imasval  17603  imasaddvallem  17621  xpsff1o  17659  catidex  17768  cidval  17771  catcocl  17779  catass  17780  oppccofval  17810  sectfval  17846  subccocl  17940  isfunc  17959  funcco  17966  idfuval  17971  idfucl  17976  cofuval  17977  cofuval2  17982  cofucl  17983  cofuass  17984  cofulid  17985  cofurid  17986  resfval  17987  resfval2  17988  funcres  17991  inclfusubc  18038  isnat  18045  nati  18053  fucco  18060  fuccoval  18061  coaval  18163  catcisolem  18205  xpcval  18271  xpcco  18277  xpcco2  18281  xpccatid  18282  xpcid  18283  1stfval  18285  2ndfval  18288  1stfcl  18291  2ndfcl  18292  prfval  18293  prf1  18294  prf2fval  18295  prf2  18296  prfcl  18297  prf1st  18298  prf2nd  18299  1st2ndprf  18300  xpcpropd  18302  evlfval  18311  evlf2  18312  evlfcllem  18315  evlfcl  18316  curfval  18317  curf1  18319  curf1cl  18322  curf2cl  18325  curfcl  18326  curfpropd  18327  uncf1  18330  uncf2  18331  curfuncf  18332  uncfcurf  18333  diagval  18334  curf2ndf  18341  hofval  18346  hof2fval  18349  hofcl  18353  yonval  18355  hofpropd  18361  yonedalem21  18367  yonedalem22  18372  yonedalem3  18374  xpsmnd0  18891  xpsinv  19189  xpsgrpsub  19190  symg2bas  19526  xpsring1d  20480  funcrngcsetc  20808  funcrngcsetcALT  20809  funcringcsetc  20842  rngqiprngimfv  21507  rngqiprngghm  21508  rngqiprngimf1  21509  rngqiprngimfo  21510  rngqiprnglin  21511  rngqipring1  21525  rngqiprngfu  21526  pzriprnglem6  21705  pzriprnglem12  21711  mat1dimmul  22704  txcnp  23852  upxp  23855  uptx  23857  hauseqlcld  23878  txlm  23880  txkgen  23884  cnmpt1t  23897  cnmpt2t  23905  txhmeo  24035  flfcnp2  24239  ucnimalem  24511  ucnima  24512  fmucndlem  24522  fmucnd  24523  cnheiborlem  25188  pi1xfrcnvlem  25290  ovollb2lem  25722  ovollb2  25723  ovolshftlem2  25744  ovolscalem2  25748  ioombl1  25796  ioorf  25807  ioorval  25808  ioorinv2  25809  uniioombllem6  25822  dyadval  25826  opnmbl  25836  mbfimaopnlem  25889  limccnp2  26126  mpodvdsmulf1o  27438  dvdsmulf1o  27440  precsexlemcbv  28479  precsexlem3  28482  seqseq123d  28559  om2noseqrdg  28577  noseqrdgsuc  28581  ebtwntg  29447  numclwwlk1lem2fv  30844  numclwwlk1lem2fo  30846  numclwwlk1lem2  30848  wlkl0  30855  hhssnvt  31754  hhsssh  31758  opsbc2ie  32959  opreu2reuALT  32960  opfv  33125  xppreima  33126  2ndresdju  33130  aciunf1lem  33143  ofpreima  33146  fgreu  33152  gsumwrd2dccatlem  33525  gsumwrd2dccat  33526  rlocval  33707  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rloc0g  33720  rloc1r  33721  rlocf1  33722  rlocinvunit  33723  rlocisunit  33724  zringfrac  33972  smatlem  34315  qtophaus  34354  qqhval2  34500  esum2dlem  34610  rrvadd  34971  hgt750lemb  35172  bnj1442  35566  bnj1450  35567  bnj1463  35572  bnj1529  35587  erdszelem9  35786  erdszelem10  35787  txpconn  35819  txsconnlem  35827  goaleq12d  35938  msubval  36112  msubco  36118  mvhval  36121  msubvrs  36147  cbvoprab123vw  36867  cbvoprab23vw  36868  cbvoprab13vw  36869  cbvopabdavw  36894  cbvoprab123davw  36902  cbvoprab12davw  36903  cbvoprab23davw  36904  cbvoprab13davw  36905  bj-dfid2ALT  37817  bj-endval  38075  finxpreclem3  38155  poimirlem4  38381  opnmbllem0  38413  mblfinlem1  38414  mblfinlem2  38415  heiborlem6  38574  heiborlem7  38575  heiborlem8  38576  nfopdALT  39852  dvhvaddcbv  41970  dvhvaddval  41971  dvhopvadd  41974  dvhvaddcomN  41977  dvhvaddass  41978  dvhvscacbv  41979  dvhvscaval  41980  dvhopvsca  41983  dvhgrp  41988  dvhlveclem  41989  dvh0g  41992  dvhopaddN  41995  dvhopspN  41996  dvhopN  41997  cdlemn4  42079  hdmapffval  42707  pellexlem3  43680  pellex  43684  elcnvlem  44449  dvnprodlem1  46782  dvnprodlem3  46784  etransclem44  47114  ovolval4  47487  ovolval5lem3  47490  aoveq123d  48074  prproropf1olem2  48412  prproropf1olem3  48413  prproropf1olem4  48414  prproropf1o  48415  prproropreud  48417  isisubgr  48786  eloprab1st2nd  49804  ssccatid  50006  oppfvalg  50060  imaf1co  50089  uptrlem1  50144  xpcfucco3  50192  dfswapf2  50195  swapfval  50196  swapfcoa  50215  1stfpropd  50224  2ndfpropd  50225  tposcurf1  50233  diag1  50238  fuco2eld2  50248  fucofvalg  50252  fuco21  50270  fuco11bALT  50272  fuco23  50275  fuco22natlem3  50278  fuco22nat  50280  fucoid  50282  fuco22a  50284  fucocolem2  50288  fucocolem4  50290  postcofval  50298  precofval  50301  precofvalALT  50302  precofval3  50305  prcofvalg  50310  prcofpropd  50313  prcofdiag1  50327  prcofdiag  50328  fucoppcco  50343  oppfdiag1  50348  oppfdiag  50350  termcfuncval  50466  diag1f1olem  50467  mndtcval  50513  mndtcco  50519  2arwcatlem2  50530  2arwcatlem3  50531  2arwcatlem4  50532  2arwcat  50534  setc1onsubc  50536  lanfval  50547  ranfval  50548  ranup  50576  concom  50597  islmd  50599