Theorem opeq12 2543

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

Syntax hints:   -> wi 3   /\ wa 230   = wceq 997  <.cop 2463

This theorem is referenced by:  opeq12i 2546  cbvopab 2727  opth 2843  copsex2g 2849  opelopabsb 2871  relop 3332  funopg 3604  fsn 3891  fnressn 3894  cbvoprab12 4056  eqop 4162  brecop 4367  th3q 4378  ecoprcom 4380  ecoprass 4381  ecoprdi 4382  xpmapenlem3 4563  mulpipq 5120  1qec 5133  halfpq 5147  prlem934a 5202  addsrpr 5249  addcnsr 5318  ax0id 5346  axcnre 5351  1ded 10753

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-v 1859  df-un 2101  df-sn 2464  df-pr 2465  df-op 2468

Copyright terms: Public domain