Theorem opeq12 4673

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507  ⟨cop 4441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442

This theorem is referenced by:  opeq12i  4676  opeq12d  4679  cbvopab  4994  opth  5219  copsex2t  5233  copsex2g  5234  relop  5565  funopg  6216  fvn0ssdmfun  6661  fsn  6714  fnressn  6737  fmptsng  6747  fmptsnd  6748  tpres  6784  cbvoprab12  7053  eqopi  7531  f1o2ndf1  7617  tposoprab  7725  omeu  8006  brecop  8184  ecovcom  8197  ecovass  8198  ecovdi  8199  xpf1o  8469  addsrmo  10287  mulsrmo  10288  addsrpr  10289  mulsrpr  10290  addcnsr  10349  axcnre  10378  seqeq1  13181  opfi1uzind  13664  fsumcnv  14982  fprodcnv  15191  eucalgval2  15775  xpstopnlem1  22115  qustgplem  22426  finsumvtxdg2size  27029  brabgaf  30117  qqhval2  30867  brsegle  33090  finxpreclem3  34115  eqrelf  34961  dvnprodlem1  41661  or2expropbilem1  42672  or2expropbilem2  42673  funop1  42888  ich2exprop  43001  ichnreuop  43002  ichreuopeq  43003  reuopreuprim  43056  uspgrsprf1  43390