Theorem opeq12d 4348

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

Syntax hints:   → wi 4   = wceq 1475  ⟨cop 4131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132

This theorem is referenced by:  nfopd  4357  moop2  4891  iunopeqop  4906  fsn2g  6311  funopsn  6319  fnprb  6377  fntpb  6378  fnpr2g  6379  fliftfuns  6464  dfmpt2  7154  fsplit  7169  fnwelem  7179  seqomlem0  7431  seqomlem1  7432  seqomlem4  7435  qliftfuns  7721  xpassen  7939  xpdom2  7940  xpf1o  8007  xpmapenlem  8012  xpmapen  8013  mapunen  8014  xpwdomg  8373  fseqenlem2  8731  nqereu  9630  addpipq2  9637  addpipq  9638  mulpipq2  9640  mulpipq  9641  1nqenq  9663  mulidnq  9664  ltexnq  9676  prlem934  9734  addsrmo  9773  mulsrmo  9774  addsrpr  9775  mulsrpr  9776  mulcnsr  9836  mulresr  9839  axcnre  9864  om2uzrdg  12617  uzrdgsuci  12621  2swrd1eqwrdeq  13306  swrdswrd0  13314  ccatopth  13322  swrdccatin2d  13351  splval  13353  splcl  13354  cshfn  13387  repswcshw  13409  2swrd2eqwrdeq  13544  ruclem1  14799  eucalgval2  15132  qnumdenbi  15290  crth  15321  phimullem  15322  prmreclem3  15460  ressval3d  15764  imasval  15994  imasaddvallem  16012  xpsff1o  16051  catidex  16158  cidval  16161  catcocl  16169  catass  16170  oppccofval  16199  sectfval  16234  subccocl  16328  isfunc  16347  funcco  16354  idfuval  16359  idfucl  16364  cofuval  16365  cofuval2  16370  cofucl  16371  cofuass  16372  cofulid  16373  cofurid  16374  resfval  16375  resfval2  16376  funcres  16379  isnat  16430  nati  16438  fucco  16445  fuccoval  16446  coaval  16541  catcisolem  16579  xpcval  16640  xpcco  16646  xpcco2  16650  xpccatid  16651  xpcid  16652  1stfval  16654  2ndfval  16657  1stfcl  16660  2ndfcl  16661  prfval  16662  prf1  16663  prf2fval  16664  prf2  16665  prfcl  16666  prf1st  16667  prf2nd  16668  1st2ndprf  16669  xpcpropd  16671  evlfval  16680  evlf2  16681  evlfcllem  16684  evlfcl  16685  curfval  16686  curf1  16688  curf1cl  16691  curf2cl  16694  curfcl  16695  curfpropd  16696  uncf1  16699  uncf2  16700  curfuncf  16701  uncfcurf  16702  diagval  16703  curf2ndf  16710  hofval  16715  hof2fval  16718  hofcl  16722  yonval  16724  hofpropd  16730  yonedalem21  16736  yonedalem22  16741  yonedalem3  16743  symg2bas  17641  mat1dimmul  20101  txcnp  21233  upxp  21236  uptx  21238  hauseqlcld  21259  txlm  21261  txkgen  21265  cnmpt1t  21278  cnmpt2t  21286  txhmeo  21416  flfcnp2  21621  ucnimalem  21894  ucnima  21895  fmucndlem  21905  fmucnd  21906  cnheiborlem  22561  pi1xfrcnvlem  22664  ovollb2lem  23063  ovollb2  23064  ovolshftlem2  23085  ovolscalem2  23089  ioombl1  23137  ioorf  23147  ioorval  23148  ioorinv2  23149  uniioombllem6  23162  dyadval  23166  opnmbl  23176  mbfimaopnlem  23228  limccnp2  23462  dvdsmulf1o  24720  ebtwntg  25662  usgrac  25880  numclwlk1lem2fv  26620  numclwlk1lem2fo  26622  hhssnvt  27506  hhsssh  27510  opfv  28828  xppreima  28829  aciunf1lem  28844  ofpreima  28848  fgreu  28854  smatlem  29191  fimaproj  29228  qtophaus  29231  qqhval2  29354  esum2dlem  29481  rrvadd  29841  bnj1442  30371  bnj1450  30372  bnj1463  30377  bnj1529  30392  erdszelem9  30435  erdszelem10  30436  txpcon  30468  txsconlem  30476  msubval  30676  msubco  30682  mvhval  30685  msubvrs  30711  finxpreclem3  32406  poimirlem4  32583  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  nfopdALT  33276  dvhvaddcbv  35396  dvhvaddval  35397  dvhopvadd  35400  dvhvaddcomN  35403  dvhvaddass  35404  dvhvscacbv  35405  dvhvscaval  35406  dvhopvsca  35409  dvhgrp  35414  dvhlveclem  35415  dvh0g  35418  dvhopaddN  35421  dvhopspN  35422  dvhopN  35423  cdlemn4  35505  hdmapffval  36136  pellexlem3  36413  pellex  36417  elcnvlem  36926  dvnprodlem1  38836  dvnprodlem3  38838  etransclem44  39171  ovolval4  39541  ovolval5lem3  39544  aoveq123d  39907  pfxsuff1eqwrdeq  40270  av-numclwlk1lem2fv  41523  av-numclwlk1lem2fo  41525  inclfusubc  41657  funcrngcsetc  41790  funcrngcsetcALT  41791  funcringcsetc  41827