Theorem opeq12 2489

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 2487	. 2 |- (A = C -> <.A, B>. = <.C, B>.)
2		opeq2 2488	. 2 |- (B = D -> <.C, B>. = <.C, D>.)
3	1, 2	sylan9eq 1527	1 |- ((A = C /\ B = D) -> <.A, B>. = <.C, D>.)

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

This theorem is referenced by:  opeq12i 2492  cbvopab 2672  opth 2787  copsex2g 2793  opabsb 2815  relop 3275  funopg 3547  fsn 3834  fnressn 3837  cbvoprab12 3998  eqop 4104  brecop 4306  th3q 4317  ecoprcom 4319  ecoprass 4320  ecoprdi 4321  xpmapenlem3 4498  mulpipq 5055  1qec 5068  halfpq 5082  prlem934a 5137  addsrpr 5184  addcnsr 5253  ax0id 5281  axcnre 5286  1ded 10671

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416

Copyright terms: Public domain