Theorem opeq12 3906

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   <.cop 3712

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718

This theorem is used by:  opeq12i  3909  opeq12d  3912  cbvopab  4202  opth  4377  copsex2t  4385  copsex2g  4386  relop  4930  funopg  5411  fsn  5880  fnressn  5901  cbvoprab12  6162  eqopi  6406  f1o2ndf1  6464  tposoprab  6551  brecop  6899  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  xpf1o  7144  1qec  7755  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  axcnre  8248  fsumcnv  12204  fprodcnv  12392  eucalgval2  12831