Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  altopth Structured version   Unicode version

Theorem altopth 30280
 Description: The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that and are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 4664), requires to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
Hypotheses
Ref Expression
altopth.1
altopth.2
Assertion
Ref Expression
altopth

Proof of Theorem altopth
StepHypRef Expression
1 altopth.1 . 2
2 altopth.2 . 2
3 altopthg 30278 . 2
41, 2, 3mp2an 670 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 367   wceq 1405   wcel 1842  cvv 3058  caltop 30267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-sn 3972  df-pr 3974  df-altop 30269 This theorem is referenced by:  altopthd  30283  altopelaltxp  30287
 Copyright terms: Public domain W3C validator