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  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  10859  frec2uzrdg  10860  frecuzrdgrcl  10861  frecuzrdgsuc  10865  frecuzrdgrclt  10866  frecuzrdgg  10867  frecuzrdgsuctlem  10874  seqeq1  10901  iseqvalcbv  10910  seq3val  10911  seqvalcd  10912  pfxsuff1eqwrdeq  11486  swrdpfx  11494  ccatopth  11503  swrdccatin2d  11531  eucalgval2  12849  qnumdenbi  12990  crth  13024  phimullem  13025  ennnfonelemg  13345  ennnfonelem1  13349  ressval3d  13477  imasex  13677  imasival  13678  imasaddvallemg  13687  xpsff1o  13721  txcnp  15424  upxp  15425  uptx  15427  txlm  15432  cnmpt1t  15438  cnmpt2t  15446  txhmeo  15472  pellexlem3  16153  mpodvdsmulf1o  16206