Theorem opeq12d 4883

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

Syntax hints:   → wi 4   = wceq 1533  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  nfopd  4892  moop2  5504  iunopeqop  5523  dfid2  5578  fsn2g  7147  funopsn  7157  fnprb  7220  fntpb  7221  fnpr2g  7222  fliftfuns  7321  dfmpo  8107  fsplit  8122  fsplitfpar  8123  fnwelem  8136  fimaproj  8140  seqomlem0  8470  seqomlem1  8471  seqomlem4  8474  qliftfuns  8823  xpassen  9091  xpdom2  9092  xpf1o  9164  xpmapenlem  9169  xpmapen  9170  mapunen  9171  xpwdomg  9610  fseqenlem2  10050  nqereu  10954  addpipq2  10961  addpipq  10962  mulpipq2  10964  mulpipq  10965  1nqenq  10987  mulidnq  10988  ltexnq  11000  prlem934  11058  addsrmo  11098  mulsrmo  11099  addsrpr  11100  mulsrpr  11101  mulcnsr  11161  mulresr  11164  axcnre  11189  om2uzrdg  13957  uzrdgsuci  13961  pfxsuff1eqwrdeq  14685  swrdpfx  14693  ccatopth  14702  swrdccatin2d  14730  splval  14737  splcl  14738  cshfn  14776  repswcshw  14798  2swrd2eqwrdeq  14940  ruclem1  16211  eucalgval2  16555  qnumdenbi  16719  crth  16750  phimullem  16751  prmreclem3  16890  setsstruct  17148  ressval3d  17230  ressval3dOLD  17231  imasval  17496  imasaddvallem  17514  xpsff1o  17552  catidex  17657  cidval  17660  catcocl  17668  catass  17669  oppccofval  17700  sectfval  17737  subccocl  17834  isfunc  17853  funcco  17860  idfuval  17865  idfucl  17870  cofuval  17871  cofuval2  17876  cofucl  17877  cofuass  17878  cofulid  17879  cofurid  17880  resfval  17881  resfval2  17882  funcres  17885  inclfusubc  17933  isnat  17940  nati  17948  fucco  17957  fuccoval  17958  coaval  18060  catcisolem  18102  xpcval  18171  xpcco  18177  xpcco2  18181  xpccatid  18182  xpcid  18183  1stfval  18185  2ndfval  18188  1stfcl  18191  2ndfcl  18192  prfval  18193  prf1  18194  prf2fval  18195  prf2  18196  prfcl  18197  prf1st  18198  prf2nd  18199  1st2ndprf  18200  xpcpropd  18203  evlfval  18212  evlf2  18213  evlfcllem  18216  evlfcl  18217  curfval  18218  curf1  18220  curf1cl  18223  curf2cl  18226  curfcl  18227  curfpropd  18228  uncf1  18231  uncf2  18232  curfuncf  18233  uncfcurf  18234  diagval  18235  curf2ndf  18242  hofval  18247  hof2fval  18250  hofcl  18254  yonval  18256  hofpropd  18262  yonedalem21  18268  yonedalem22  18273  yonedalem3  18275  xpsmnd0  18738  xpsinv  19024  xpsgrpsub  19025  symg2bas  19359  xpsring1d  20281  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  rngqiprngimfv  21205  rngqiprngghm  21206  rngqiprngimf1  21207  rngqiprngimfo  21208  rngqiprnglin  21209  rngqipring1  21223  rngqiprngfu  21224  pzriprnglem6  21429  pzriprnglem12  21435  mat1dimmul  22422  txcnp  23568  upxp  23571  uptx  23573  hauseqlcld  23594  txlm  23596  txkgen  23600  cnmpt1t  23613  cnmpt2t  23621  txhmeo  23751  flfcnp2  23955  ucnimalem  24229  ucnima  24230  fmucndlem  24240  fmucnd  24241  cnheiborlem  24924  pi1xfrcnvlem  25027  ovollb2lem  25461  ovollb2  25462  ovolshftlem2  25483  ovolscalem2  25487  ioombl1  25535  ioorf  25546  ioorval  25547  ioorinv2  25548  uniioombllem6  25561  dyadval  25565  opnmbl  25575  mbfimaopnlem  25628  limccnp2  25865  mpodvdsmulf1o  27171  dvdsmulf1o  27173  precsexlemcbv  28154  precsexlem3  28157  seqseq123d  28209  om2noseqrdg  28227  noseqrdgsuc  28231  ebtwntg  28865  numclwwlk1lem2fv  30238  numclwwlk1lem2fo  30240  numclwwlk1lem2  30242  wlkl0  30249  hhssnvt  31147  hhsssh  31151  opsbc2ie  32352  opreu2reuALT  32353  opfv  32512  xppreima  32513  2ndresdju  32516  aciunf1lem  32529  ofpreima  32532  fgreu  32539  rlocval  33049  rlocaddval  33058  rlocmulval  33059  rloccring  33060  rloc0g  33061  rloc1r  33062  rlocf1  33063  zringfrac  33366  smatlem  33526  qtophaus  33565  qqhval2  33711  esum2dlem  33839  rrvadd  34200  hgt750lemb  34416  bnj1442  34808  bnj1450  34809  bnj1463  34814  bnj1529  34829  swrdrevpfx  34854  erdszelem9  34937  erdszelem10  34938  txpconn  34970  txsconnlem  34978  goaleq12d  35089  msubval  35263  msubco  35269  mvhval  35272  msubvrs  35298  bj-dfid2ALT  36672  bj-endval  36922  finxpreclem3  37000  poimirlem4  37225  opnmbllem0  37257  mblfinlem1  37258  mblfinlem2  37259  heiborlem6  37417  heiborlem7  37418  heiborlem8  37419  nfopdALT  38570  dvhvaddcbv  40689  dvhvaddval  40690  dvhopvadd  40693  dvhvaddcomN  40696  dvhvaddass  40697  dvhvscacbv  40698  dvhvscaval  40699  dvhopvsca  40702  dvhgrp  40707  dvhlveclem  40708  dvh0g  40711  dvhopaddN  40714  dvhopspN  40715  dvhopN  40716  cdlemn4  40798  hdmapffval  41426  pellexlem3  42390  pellex  42394  elcnvlem  43170  dvnprodlem1  45469  dvnprodlem3  45471  etransclem44  45801  ovolval4  46174  ovolval5lem3  46177  aoveq123d  46693  prproropf1olem2  46978  prproropf1olem3  46979  prproropf1olem4  46980  prproropf1o  46981  prproropreud  46983  isisubgr  47331  mndtcval  48274  mndtcco  48280