Theorem opeq12 3827

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  ⟨cop 3641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647

This theorem is referenced by:  opeq12i  3830  opeq12d  3833  cbvopab  4123  opth  4289  copsex2t  4297  copsex2g  4298  relop  4836  funopg  5314  fsn  5765  fnressn  5783  cbvoprab12  6032  eqopi  6271  f1o2ndf1  6327  tposoprab  6379  brecop  6725  th3q  6740  ecovcom  6742  ecovicom  6743  ecovass  6744  ecoviass  6745  ecovdi  6746  ecovidi  6747  xpf1o  6956  1qec  7521  enq0sym  7565  addnq0mo  7580  mulnq0mo  7581  addnnnq0  7582  mulnnnq0  7583  distrnq0  7592  mulcomnq0  7593  addassnq0  7595  addsrmo  7876  mulsrmo  7877  addsrpr  7878  mulsrpr  7879  axcnre  8014  fsumcnv  11823  fprodcnv  12011  eucalgval2  12450