Theorem opeq12 4842

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opeq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Proof of Theorem opeq12

Step	Hyp	Ref	Expression
1		opeq1 4840	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 4841	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2785	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⟨cop 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  opeq12i  4845  opeq12d  4848  cbvopab  5182  cbvopabv  5183  opth  5439  copsex2t  5455  relop  5817  funopg  6553  fvn0ssdmfun  7049  fsn  7110  fnressn  7133  fmptsng  7145  fmptsnd  7146  tpres  7178  cbvoprab12  7481  cbvoprab12v  7482  eqopi  8007  f1o2ndf1  8104  tposoprab  8244  omeu  8552  brecop  8786  ecovcom  8799  ecovass  8800  ecovdi  8801  xpf1o  9109  addsrmo  11033  mulsrmo  11034  addsrpr  11035  mulsrpr  11036  addcnsr  11095  axcnre  11124  seqeq1  13976  opfi1uzind  14483  fsumcnv  15746  fprodcnv  15956  eucalgval2  16558  xpstopnlem1  23703  qustgplem  24015  finsumvtxdg2size  29485  brabgaf  32543  qqhval2  33979  brsegle  36103  copsex2d  37134  finxpreclem3  37388  eqrelf  38251  dvnprodlem1  45951  or2expropbilem1  47037  or2expropbilem2  47038  funop1  47288  ich2exprop  47476  ichnreuop  47477  ichreuopeq  47478  reuopreuprim  47531  uspgrsprf1  48139