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	⊢ (𝜑 → 𝐴 = 𝐵)
opeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
opeq12d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		opeq12 3906	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

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  10847  frec2uzrdg  10848  frecuzrdgrcl  10849  frecuzrdgsuc  10853  frecuzrdgrclt  10854  frecuzrdgg  10855  frecuzrdgsuctlem  10862  seqeq1  10889  iseqvalcbv  10898  seq3val  10899  seqvalcd  10900  pfxsuff1eqwrdeq  11473  swrdpfx  11481  ccatopth  11490  swrdccatin2d  11518  eucalgval2  12833  qnumdenbi  12972  crth  13004  phimullem  13005  ennnfonelemg  13296  ennnfonelem1  13300  ressval3d  13428  imasex  13628  imasival  13629  imasaddvallemg  13638  xpsff1o  13672  txcnp  15374  upxp  15375  uptx  15377  txlm  15382  cnmpt1t  15388  cnmpt2t  15396  txhmeo  15422  pellexlem3  16099  mpodvdsmulf1o  16110