Theorem opeq12d 3912

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	|- ( ph -> A = B )
opeq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
opeq12d	|- ( ph -> <. A , C >. = <. B , D >. )

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 |- ( ph -> A = B )
2		opeq12d.2	. 2 |- ( ph -> C = D )
3		opeq12 3906	. 2 |- ( ( A = B /\ C = D ) -> <. A , C >. = <. B , D >. )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> <. A , C >. = <. B , D >. )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   <.cop 3712

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718

This theorem is used by:  nfopd  3921  moop2  4392  fsn2g  5883  funopsn  5891  fliftfuns  6004  elxp6  6403  dfmpo  6459  tfrlemi1  6603  qliftfuns  6893  xpassen  7128  xpdom2  7129  xpf1o  7144  xpmapenlem  7149  xpmapen  7150  mapunen  7151  dfplpq2  7722  dfmpq2  7723  addpipqqs  7738  mulpipq2  7739  mulpipq  7740  mulpipqqs  7741  mulidnq  7757  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  nqnq0a  7822  nqnq0m  7823  nq0a0  7825  nq02m  7833  genpdf  7876  genipv  7877  genpelxp  7879  addcomprg  7946  mulcomprg  7948  prplnqu  7988  cauappcvgprlemlim  8029  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  caucvgsr  8170  addcnsr  8202  mulcnsr  8203  mulresr  8206  pitonnlem2  8215  pitonn  8216  recidpipr  8224  axaddcom  8238  ax0id  8246  axcnre  8249  nntopi  8262  axcaucvglemval  8265  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgsuctlem  10875  seqeq1  10902  iseqvalcbv  10911  seq3val  10912  seqvalcd  10913  pfxsuff1eqwrdeq  11487  swrdpfx  11495  ccatopth  11504  swrdccatin2d  11532  eucalgval2  12850  qnumdenbi  12991  crth  13025  phimullem  13026  ennnfonelemg  13346  ennnfonelem1  13350  ressval3d  13479  imasex  13679  imasival  13680  imasaddvallemg  13689  xpsff1o  13723  txcnp  15463  upxp  15464  uptx  15466  txlm  15471  cnmpt1t  15477  cnmpt2t  15485  txhmeo  15511  pellexlem3  16192  mpodvdsmulf1o  16245