Theorem opeq12 2485

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

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

This theorem is referenced by:  opeq12i 2488  cbvopab 2667  opth 2782  copsex2g 2788  opabsb 2810  relop 3270  funopg 3539  fsn 3825  fnressn 3828  cbvoprab12 3989  eqop 4094  brecop 4296  th3q 4307  ecoprcom 4309  ecoprass 4310  ecoprdi 4311  xpmapenlem3 4484  mulpipq 5035  1qec 5048  halfpq 5062  prlem934a 5117  addsrpr 5164  addcnsr 5233  ax0id 5261  axcnre 5266  1ded 10551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412

Copyright terms: Public domain