MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfop Structured version   Unicode version

Theorem dfop 4212
Description: Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.)
Hypotheses
Ref Expression
dfop.1  |-  A  e. 
_V
dfop.2  |-  B  e. 
_V
Assertion
Ref Expression
dfop  |-  <. A ,  B >.  =  { { A } ,  { A ,  B } }

Proof of Theorem dfop
StepHypRef Expression
1 dfop.1 . 2  |-  A  e. 
_V
2 dfop.2 . 2  |-  B  e. 
_V
3 dfopg 4211 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  -> 
<. A ,  B >.  =  { { A } ,  { A ,  B } } )
41, 2, 3mp2an 672 1  |-  <. A ,  B >.  =  { { A } ,  { A ,  B } }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767   _Vcvv 3113   {csn 4027   {cpr 4029   <.cop 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-op 4034
This theorem is referenced by:  opid  4232  elop  4713  opi1  4714  opi2  4715  op1stb  4717  opeqsn  4743  opeqpr  4744  uniop  4750  xpsspw  5114  xpsspwOLD  5115  relop  5151  funopg  5618
  Copyright terms: Public domain W3C validator