Theorem opeq12d 4778

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

Syntax hints:   → wi 4   = wceq 1543  ⟨cop 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534

This theorem is referenced by:  nfopd  4787  moop2  5370  iunopeqop  5389  fsn2g  6931  funopsn  6941  fnprb  7002  fntpb  7003  fnpr2g  7004  fliftfuns  7101  dfmpo  7848  fsplit  7863  fsplitOLD  7864  fsplitfpar  7865  fnwelem  7876  fimaproj  7880  seqomlem0  8163  seqomlem1  8164  seqomlem4  8167  qliftfuns  8464  xpassen  8717  xpdom2  8718  xpf1o  8786  xpmapenlem  8791  xpmapen  8792  mapunen  8793  xpwdomg  9179  fseqenlem2  9604  nqereu  10508  addpipq2  10515  addpipq  10516  mulpipq2  10518  mulpipq  10519  1nqenq  10541  mulidnq  10542  ltexnq  10554  prlem934  10612  addsrmo  10652  mulsrmo  10653  addsrpr  10654  mulsrpr  10655  mulcnsr  10715  mulresr  10718  axcnre  10743  om2uzrdg  13494  uzrdgsuci  13498  pfxsuff1eqwrdeq  14229  swrdpfx  14237  ccatopth  14246  swrdccatin2d  14274  splval  14281  splcl  14282  cshfn  14320  repswcshw  14342  2swrd2eqwrdeq  14483  ruclem1  15755  eucalgval2  16101  qnumdenbi  16263  crth  16294  phimullem  16295  prmreclem3  16434  setsstruct  16705  ressval3d  16745  imasval  16970  imasaddvallem  16988  xpsff1o  17026  catidex  17131  cidval  17134  catcocl  17142  catass  17143  oppccofval  17174  sectfval  17210  subccocl  17305  isfunc  17324  funcco  17331  idfuval  17336  idfucl  17341  cofuval  17342  cofuval2  17347  cofucl  17348  cofuass  17349  cofulid  17350  cofurid  17351  resfval  17352  resfval2  17353  funcres  17356  isnat  17408  nati  17416  fucco  17425  fuccoval  17426  coaval  17528  catcisolem  17570  xpcval  17638  xpcco  17644  xpcco2  17648  xpccatid  17649  xpcid  17650  1stfval  17652  2ndfval  17655  1stfcl  17658  2ndfcl  17659  prfval  17660  prf1  17661  prf2fval  17662  prf2  17663  prfcl  17664  prf1st  17665  prf2nd  17666  1st2ndprf  17667  xpcpropd  17670  evlfval  17679  evlf2  17680  evlfcllem  17683  evlfcl  17684  curfval  17685  curf1  17687  curf1cl  17690  curf2cl  17693  curfcl  17694  curfpropd  17695  uncf1  17698  uncf2  17699  curfuncf  17700  uncfcurf  17701  diagval  17702  curf2ndf  17709  hofval  17714  hof2fval  17717  hofcl  17721  yonval  17723  hofpropd  17729  yonedalem21  17735  yonedalem22  17740  yonedalem3  17742  symg2bas  18739  mat1dimmul  21327  txcnp  22471  upxp  22474  uptx  22476  hauseqlcld  22497  txlm  22499  txkgen  22503  cnmpt1t  22516  cnmpt2t  22524  txhmeo  22654  flfcnp2  22858  ucnimalem  23131  ucnima  23132  fmucndlem  23142  fmucnd  23143  cnheiborlem  23805  pi1xfrcnvlem  23907  ovollb2lem  24339  ovollb2  24340  ovolshftlem2  24361  ovolscalem2  24365  ioombl1  24413  ioorf  24424  ioorval  24425  ioorinv2  24426  uniioombllem6  24439  dyadval  24443  opnmbl  24453  mbfimaopnlem  24506  limccnp2  24743  dvdsmulf1o  26030  ebtwntg  27027  numclwwlk1lem2fv  28393  numclwwlk1lem2fo  28395  numclwwlk1lem2  28397  wlkl0  28404  hhssnvt  29300  hhsssh  29304  opsbc2ie  30497  opreu2reuALT  30498  opfv  30655  xppreima  30656  2ndresdju  30659  aciunf1lem  30673  ofpreima  30676  fgreu  30683  smatlem  31415  qtophaus  31454  qqhval2  31598  esum2dlem  31726  rrvadd  32085  hgt750lemb  32302  bnj1442  32696  bnj1450  32697  bnj1463  32702  bnj1529  32717  swrdrevpfx  32745  erdszelem9  32828  erdszelem10  32829  txpconn  32861  txsconnlem  32869  goaleq12d  32980  msubval  33154  msubco  33160  mvhval  33163  msubvrs  33189  bj-endval  35169  finxpreclem3  35250  poimirlem4  35467  opnmbllem0  35499  mblfinlem1  35500  mblfinlem2  35501  heiborlem6  35660  heiborlem7  35661  heiborlem8  35662  nfopdALT  36671  dvhvaddcbv  38789  dvhvaddval  38790  dvhopvadd  38793  dvhvaddcomN  38796  dvhvaddass  38797  dvhvscacbv  38798  dvhvscaval  38799  dvhopvsca  38802  dvhgrp  38807  dvhlveclem  38808  dvh0g  38811  dvhopaddN  38814  dvhopspN  38815  dvhopN  38816  cdlemn4  38898  hdmapffval  39526  pellexlem3  40297  pellex  40301  elcnvlem  40826  dvnprodlem1  43105  dvnprodlem3  43107  etransclem44  43437  ovolval4  43807  ovolval5lem3  43810  aoveq123d  44285  prproropf1olem2  44572  prproropf1olem3  44573  prproropf1olem4  44574  prproropf1o  44575  prproropreud  44577  inclfusubc  45041  funcrngcsetc  45172  funcrngcsetcALT  45173  funcringcsetc  45209  mndtcval  45980  mndtcco  45986