Theorem opeq12d 4685

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

Syntax hints:   → wi 4   = wceq 1507  ⟨cop 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448

This theorem is referenced by:  nfopd  4694  moop2  5248  iunopeqop  5267  fsn2g  6723  funopsn  6733  fnprb  6797  fntpb  6798  fnpr2g  6799  fliftfuns  6890  dfmpo  7605  fsplit  7620  fnwelem  7630  seqomlem0  7888  seqomlem1  7889  seqomlem4  7892  qliftfuns  8184  xpassen  8407  xpdom2  8408  xpf1o  8475  xpmapenlem  8480  xpmapen  8481  mapunen  8482  xpwdomg  8844  fseqenlem2  9245  nqereu  10149  addpipq2  10156  addpipq  10157  mulpipq2  10159  mulpipq  10160  1nqenq  10182  mulidnq  10183  ltexnq  10195  prlem934  10253  addsrmo  10293  mulsrmo  10294  addsrpr  10295  mulsrpr  10296  mulcnsr  10356  mulresr  10359  axcnre  10384  om2uzrdg  13139  uzrdgsuci  13143  2swrd1eqwrdeqOLD  13847  pfxsuff1eqwrdeq  13881  swrdswrd0OLD  13890  swrdpfx  13891  ccatopth  13907  ccatopthOLD  13908  swrdccatin2d  13952  splvalpfxOLD  13962  splval  13963  splvalOLD  13964  splcl  13965  splclOLD  13966  cshfn  14011  cshfnOLD  14012  repswcshw  14036  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  ruclem1  15444  eucalgval2  15781  qnumdenbi  15940  crth  15971  phimullem  15972  prmreclem3  16110  setsstruct  16379  ressval3d  16417  imasval  16640  imasaddvallem  16658  xpsff1o  16697  catidex  16803  cidval  16806  catcocl  16814  catass  16815  oppccofval  16844  sectfval  16879  subccocl  16973  isfunc  16992  funcco  16999  idfuval  17004  idfucl  17009  cofuval  17010  cofuval2  17015  cofucl  17016  cofuass  17017  cofulid  17018  cofurid  17019  resfval  17020  resfval2  17021  funcres  17024  isnat  17075  nati  17083  fucco  17090  fuccoval  17091  coaval  17186  catcisolem  17224  xpcval  17285  xpcco  17291  xpcco2  17295  xpccatid  17296  xpcid  17297  1stfval  17299  2ndfval  17302  1stfcl  17305  2ndfcl  17306  prfval  17307  prf1  17308  prf2fval  17309  prf2  17310  prfcl  17311  prf1st  17312  prf2nd  17313  1st2ndprf  17314  xpcpropd  17316  evlfval  17325  evlf2  17326  evlfcllem  17329  evlfcl  17330  curfval  17331  curf1  17333  curf1cl  17336  curf2cl  17339  curfcl  17340  curfpropd  17341  uncf1  17344  uncf2  17345  curfuncf  17346  uncfcurf  17347  diagval  17348  curf2ndf  17355  hofval  17360  hof2fval  17363  hofcl  17367  yonval  17369  hofpropd  17375  yonedalem21  17381  yonedalem22  17386  yonedalem3  17388  symg2bas  18287  mat1dimmul  20789  txcnp  21932  upxp  21935  uptx  21937  hauseqlcld  21958  txlm  21960  txkgen  21964  cnmpt1t  21977  cnmpt2t  21985  txhmeo  22115  flfcnp2  22319  ucnimalem  22592  ucnima  22593  fmucndlem  22603  fmucnd  22604  cnheiborlem  23261  pi1xfrcnvlem  23363  ovollb2lem  23792  ovollb2  23793  ovolshftlem2  23814  ovolscalem2  23818  ioombl1  23866  ioorf  23877  ioorval  23878  ioorinv2  23879  uniioombllem6  23892  dyadval  23896  opnmbl  23906  mbfimaopnlem  23959  limccnp2  24193  dvdsmulf1o  25473  ebtwntg  26471  numclwwlk1lem2fv  27898  numclwwlk1lem2fo  27900  numclwwlk1lem2fvOLD  27903  numclwwlk1lem2foOLD  27905  numclwwlk1lem2  27907  numclwwlk1lem2OLD  27908  wlkl0  27920  hhssnvt  28821  hhsssh  28825  opsbc2ie  30021  opreu2reuALT  30022  opfv  30155  xppreima  30156  aciunf1lem  30169  ofpreima  30172  fgreu  30179  smatlem  30701  fimaproj  30738  qtophaus  30741  qqhval2  30864  esum2dlem  30992  rrvadd  31353  hgt750lemb  31572  bnj1442  31963  bnj1450  31964  bnj1463  31969  bnj1529  31984  erdszelem9  32028  erdszelem10  32029  txpconn  32061  txsconnlem  32069  goaleq12d  32177  msubval  32289  msubco  32295  mvhval  32298  msubvrs  32324  finxpreclem3  34112  poimirlem4  34334  opnmbllem0  34366  mblfinlem1  34367  mblfinlem2  34368  heiborlem6  34533  heiborlem7  34534  heiborlem8  34535  nfopdALT  35549  dvhvaddcbv  37667  dvhvaddval  37668  dvhopvadd  37671  dvhvaddcomN  37674  dvhvaddass  37675  dvhvscacbv  37676  dvhvscaval  37677  dvhopvsca  37680  dvhgrp  37685  dvhlveclem  37686  dvh0g  37689  dvhopaddN  37692  dvhopspN  37693  dvhopN  37694  cdlemn4  37776  hdmapffval  38404  pellexlem3  38821  pellex  38825  elcnvlem  39320  dvnprodlem1  41659  dvnprodlem3  41661  etransclem44  41992  ovolval4  42362  ovolval5lem3  42365  aoveq123d  42781  prproropf1olem2  43032  prproropf1olem3  43033  prproropf1olem4  43034  prproropf1o  43035  prproropreud  43037  inclfusubc  43500  funcrngcsetc  43631  funcrngcsetcALT  43632  funcringcsetc  43668