Theorem opeq12 3592

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)

Assertion

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

Proof of Theorem opeq12

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1285   <.cop 3419

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2612  df-un 2986  df-sn 3422  df-pr 3423  df-op 3425

This theorem is referenced by:  opeq12i  3595  opeq12d  3598  cbvopab  3869  opth  4020  copsex2t  4028  copsex2g  4029  relop  4534  funopg  4984  fsn  5388  fnressn  5402  cbvoprab12  5630  eqopi  5850  f1o2ndf1  5901  tposoprab  5950  brecop  6284  th3q  6299  ecovcom  6301  ecovicom  6302  ecovass  6303  ecoviass  6304  ecovdi  6305  ecovidi  6306  xpf1o  6407  1qec  6710  enq0sym  6754  addnq0mo  6769  mulnq0mo  6770  addnnnq0  6771  mulnnnq0  6772  distrnq0  6781  mulcomnq0  6782  addassnq0  6784  addsrmo  7052  mulsrmo  7053  addsrpr  7054  mulsrpr  7055  axcnre  7179  eucalgval2  10660