ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq12 Unicode version

Theorem opeq12 3675
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
StepHypRef Expression
1 opeq1 3673 . 2  |-  ( A  =  C  ->  <. A ,  B >.  =  <. C ,  B >. )
2 opeq2 3674 . 2  |-  ( B  =  D  ->  <. C ,  B >.  =  <. C ,  D >. )
31, 2sylan9eq 2168 1  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1314   <.cop 3498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504
This theorem is referenced by:  opeq12i  3678  opeq12d  3681  cbvopab  3967  opth  4127  copsex2t  4135  copsex2g  4136  relop  4657  funopg  5125  fsn  5558  fnressn  5572  cbvoprab12  5811  eqopi  6036  f1o2ndf1  6091  tposoprab  6143  brecop  6485  th3q  6500  ecovcom  6502  ecovicom  6503  ecovass  6504  ecoviass  6505  ecovdi  6506  ecovidi  6507  xpf1o  6704  1qec  7160  enq0sym  7204  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  mulnnnq0  7222  distrnq0  7231  mulcomnq0  7232  addassnq0  7234  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  axcnre  7653  fsumcnv  11157  eucalgval2  11641
  Copyright terms: Public domain W3C validator