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  7721  dfmpq2  7722  addpipqqs  7737  mulpipq2  7738  mulpipq  7739  mulpipqqs  7740  mulidnq  7756  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  nqnq0a  7821  nqnq0m  7822  nq0a0  7824  nq02m  7832  genpdf  7875  genipv  7876  genpelxp  7878  addcomprg  7945  mulcomprg  7947  prplnqu  7987  cauappcvgprlemlim  8028  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  caucvgsr  8169  addcnsr  8201  mulcnsr  8202  mulresr  8205  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axaddcom  8237  ax0id  8245  axcnre  8248  nntopi  8261  axcaucvglemval  8264  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgsuctlem  10860  seqeq1  10887  iseqvalcbv  10896  seq3val  10897  seqvalcd  10898  pfxsuff1eqwrdeq  11471  swrdpfx  11479  ccatopth  11488  swrdccatin2d  11516  eucalgval2  12831  qnumdenbi  12970  crth  13002  phimullem  13003  ennnfonelemg  13294  ennnfonelem1  13298  ressval3d  13426  imasex  13626  imasival  13627  imasaddvallemg  13636  xpsff1o  13670  txcnp  15372  upxp  15373  uptx  15375  txlm  15380  cnmpt1t  15386  cnmpt2t  15394  txhmeo  15420  pellexlem3  16093  mpodvdsmulf1o  16104