Theorem opeq12d 4841

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  nfopd  4850  moop2  5474  iunopeqop  5494  iunopeqopOLD  5495  dfid2  5548  fsn2g  7131  funopsn  7143  funopsnOLD  7144  fnprb  7206  fntpb  7207  fnpr2g  7208  fliftfuns  7314  dfmpo  8102  fsplit  8117  fsplitfpar  8118  fnwelem  8132  fimaproj  8136  seqomlem0  8443  seqomlem1  8444  seqomlem4  8447  qliftfuns  8809  xpassen  9074  xpdom2  9075  xpf1o  9142  xpmapenlem  9147  xpmapen  9148  mapunen  9149  xpwdomg  9563  fseqenlem2  10085  nqereu  10995  addpipq2  11002  addpipq  11003  mulpipq2  11005  mulpipq  11006  1nqenq  11028  mulidnq  11029  ltexnq  11041  prlem934  11099  addsrmo  11139  mulsrmo  11140  addsrpr  11141  mulsrpr  11142  mulcnsr  11202  mulresr  11205  axcnre  11230  om2uzrdg  14079  uzrdgsuci  14083  pfxsuff1eqwrdeq  14828  swrdpfx  14836  ccatopth  14845  swrdccatin2d  14873  splval  14880  splcl  14881  swrdrevpfx  14898  cshfn  14921  repswcshw  14943  2swrd2eqwrdeq  15086  ruclem1  16379  eucalgval2  16736  qnumdenbi  16900  crth  16935  phimullem  16936  prmreclem3  17076  setsstruct  17334  ressval3d  17404  imasval  17663  imasaddvallem  17681  xpsff1o  17719  catidex  17828  cidval  17831  catcocl  17839  catass  17840  oppccofval  17870  sectfval  17906  subccocl  18000  isfunc  18019  funcco  18026  idfuval  18031  idfucl  18036  cofuval  18037  cofuval2  18042  cofucl  18043  cofuass  18044  cofulid  18045  cofurid  18046  resfval  18047  resfval2  18048  funcres  18051  inclfusubc  18098  isnat  18105  nati  18113  fucco  18120  fuccoval  18121  coaval  18223  catcisolem  18265  xpcval  18331  xpcco  18337  xpcco2  18341  xpccatid  18342  xpcid  18343  1stfval  18345  2ndfval  18348  1stfcl  18351  2ndfcl  18352  prfval  18353  prf1  18354  prf2fval  18355  prf2  18356  prfcl  18357  prf1st  18358  prf2nd  18359  1st2ndprf  18360  xpcpropd  18362  evlfval  18371  evlf2  18372  evlfcllem  18375  evlfcl  18376  curfval  18377  curf1  18379  curf1cl  18382  curf2cl  18385  curfcl  18386  curfpropd  18387  uncf1  18390  uncf2  18391  curfuncf  18392  uncfcurf  18393  diagval  18394  curf2ndf  18401  hofval  18406  hof2fval  18409  hofcl  18413  yonval  18415  hofpropd  18421  yonedalem21  18427  yonedalem22  18432  yonedalem3  18434  xpsmnd0  18952  xpsinv  19250  xpsgrpsub  19251  symg2bas  19587  xpsring1d  20543  funcrngcsetc  20872  funcrngcsetcALT  20873  funcringcsetc  20906  rngqiprngimfv  21574  rngqiprngghm  21575  rngqiprngimf1  21576  rngqiprngimfo  21577  rngqiprnglin  21578  rngqipring1  21592  rngqiprngfu  21593  pzriprnglem6  21772  pzriprnglem12  21778  mat1dimmul  22771  txcnp  23919  upxp  23922  uptx  23924  hauseqlcld  23945  txlm  23947  txkgen  23951  cnmpt1t  23964  cnmpt2t  23972  txhmeo  24102  flfcnp2  24306  ucnimalem  24578  ucnima  24579  fmucndlem  24589  fmucnd  24590  cnheiborlem  25255  pi1xfrcnvlem  25357  ovollb2lem  25789  ovollb2  25790  ovolshftlem2  25811  ovolscalem2  25815  ioombl1  25863  ioorf  25874  ioorval  25875  ioorinv2  25876  uniioombllem6  25889  dyadval  25893  opnmbl  25903  mbfimaopnlem  25956  limccnp2  26192  mpodvdsmulf1o  27503  dvdsmulf1o  27505  precsexlemcbv  28574  precsexlem3  28577  seqseq123d  28654  om2noseqrdg  28672  noseqrdgsuc  28676  ebtwntg  29542  numclwwlk1lem2fv  30939  numclwwlk1lem2fo  30941  numclwwlk1lem2  30943  wlkl0  30950  hhssnvt  31849  hhsssh  31853  opsbc2ie  33054  opreu2reuALT  33055  opfv  33220  xppreima  33221  2ndresdju  33225  aciunf1lem  33238  ofpreima  33241  fgreu  33247  gsumwrd2dccatlem  33620  gsumwrd2dccat  33621  rlocval  33802  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rloc0g  33815  rloc1r  33816  rlocf1  33817  rlocinvunit  33818  rlocisunit  33819  zringfrac  34068  smatlem  34411  qtophaus  34450  qqhval2  34596  esum2dlem  34706  rrvadd  35067  hgt750lemb  35268  bnj1442  35662  bnj1450  35663  bnj1463  35668  bnj1529  35683  erdszelem9  35933  erdszelem10  35934  txpconn  35966  txsconnlem  35974  goaleq12d  36085  msubval  36259  msubco  36265  mvhval  36268  msubvrs  36294  cbvoprab123vw  36998  cbvoprab23vw  36999  cbvoprab13vw  37000  cbvopabdavw  37025  cbvoprab123davw  37033  cbvoprab12davw  37034  cbvoprab23davw  37035  cbvoprab13davw  37036  bj-dfid2ALT  37948  bj-endval  38204  finxpreclem3  38284  poimirlem4  38510  opnmbllem0  38542  mblfinlem1  38543  mblfinlem2  38544  heiborlem6  38718  heiborlem7  38719  heiborlem8  38720  nfopdALT  39996  dvhvaddcbv  42114  dvhvaddval  42115  dvhopvadd  42118  dvhvaddcomN  42121  dvhvaddass  42122  dvhvscacbv  42123  dvhvscaval  42124  dvhopvsca  42127  dvhgrp  42132  dvhlveclem  42133  dvh0g  42136  dvhopaddN  42139  dvhopspN  42140  dvhopN  42141  cdlemn4  42223  hdmapffval  42851  pellexlem3  43791  pellex  43795  elcnvlem  44560  dvnprodlem1  46900  dvnprodlem3  46902  etransclem44  47232  ovolval4  47605  ovolval5lem3  47608  aoveq123d  48192  prproropf1olem2  48530  prproropf1olem3  48531  prproropf1olem4  48532  prproropf1o  48533  prproropreud  48535  isisubgr  48904  eloprab1st2nd  49922  ssccatid  50124  oppfvalg  50178  imaf1co  50207  uptrlem1  50262  xpcfucco3  50310  dfswapf2  50313  swapfval  50314  swapfcoa  50333  1stfpropd  50342  2ndfpropd  50343  tposcurf1  50351  diag1  50356  fuco2eld2  50366  fucofvalg  50370  fuco21  50388  fuco11bALT  50390  fuco23  50393  fuco22natlem3  50396  fuco22nat  50398  fucoid  50400  fuco22a  50402  fucocolem2  50406  fucocolem4  50408  postcofval  50416  precofval  50419  precofvalALT  50420  precofval3  50423  prcofvalg  50428  prcofpropd  50431  prcofdiag1  50445  prcofdiag  50446  fucoppcco  50461  oppfdiag1  50466  oppfdiag  50468  termcfuncval  50584  diag1f1olem  50585  mndtcval  50631  mndtcco  50637  2arwcatlem2  50648  2arwcatlem3  50649  2arwcatlem4  50650  2arwcat  50652  setc1onsubc  50654  lanfval  50665  ranfval  50666  ranup  50694  concom  50715  islmd  50717