Theorem opeq12 4404

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 4402	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 4403	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2676	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ⟨cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  opeq12i  4407  opeq12d  4410  cbvopab  4721  opth  4945  copsex2t  4957  copsex2g  4958  relop  5272  funopg  5922  fvn0ssdmfun  6350  fsn  6402  fnressn  6425  fmptsng  6434  fmptsnd  6435  tpres  6466  cbvoprab12  6729  eqopi  7202  f1o2ndf1  7285  tposoprab  7388  omeu  7665  brecop  7840  ecovcom  7854  ecovass  7855  ecovdi  7856  xpf1o  8122  addsrmo  9894  mulsrmo  9895  addsrpr  9896  mulsrpr  9897  addcnsr  9956  axcnre  9985  seqeq1  12804  opfi1uzind  13283  opfi1uzindOLD  13289  fsumcnv  14504  fprodcnv  14713  eucalgval2  15294  xpstopnlem1  21612  qustgplem  21924  finsumvtxdg2size  26446  brabgaf  29420  qqhval2  30026  brsegle  32215  finxpreclem3  33230  eqrelf  34020  dvnprodlem1  40161  funop1  41302  uspgrsprf1  41755