Theorem opeq12 2480

Description: Equality theorem for ordered pairs.

Assertion

Ref	Expression
opeq12	|- ((A = C /\ B = D) -> <.A, B>. = <.C, D>.)

Proof of Theorem opeq12

Step	Hyp	Ref	Expression
1		opeq1 2478	. 2 |- (A = C -> <.A, B>. = <.C, B>.)
2		opeq2 2479	. 2 |- (B = D -> <.C, B>. = <.C, D>.)
3	1, 2	sylan9eq 1519	1 |- ((A = C /\ B = D) -> <.A, B>. = <.C, D>.)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953  <.cop 2401

This theorem is referenced by:  opeq12i 2483  cbvopab 2662  opth 2777  copsex2g 2783  opabsb 2804  relop 3265  funopg 3533  fsn 3819  fnressn 3822  cbvoprab12 3983  eqop 4088  brecop 4290  th3q 4301  ecoprcom 4303  ecoprass 4304  ecoprdi 4305  xpmapenlem3 4478  mulpipq 5027  1qec 5040  halfpq 5054  prlem934a 5109  addsrpr 5156  addcnsr 5225  ax0id 5253  axcnre 5258  1ded 10515

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406

Copyright terms: Public domain