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

Theorem opelres 4934
Description: Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)
Hypothesis
Ref Expression
opelres.1  |-  B  e. 
_V
Assertion
Ref Expression
opelres  |-  ( <. A ,  B >.  e.  ( C  |`  D )  <-> 
( <. A ,  B >.  e.  C  /\  A  e.  D ) )

Proof of Theorem opelres
StepHypRef Expression
1 df-res 4667 . . 3  |-  ( C  |`  D )  =  ( C  i^i  ( D  X.  _V ) )
21eleq2i 2320 . 2  |-  ( <. A ,  B >.  e.  ( C  |`  D )  <->  <. A ,  B >.  e.  ( C  i^i  ( D  X.  _V ) ) )
3 elin 3319 . 2  |-  ( <. A ,  B >.  e.  ( C  i^i  ( D  X.  _V ) )  <-> 
( <. A ,  B >.  e.  C  /\  <. A ,  B >.  e.  ( D  X.  _V )
) )
4 opelres.1 . . . 4  |-  B  e. 
_V
5 opelxp 4693 . . . 4  |-  ( <. A ,  B >.  e.  ( D  X.  _V ) 
<->  ( A  e.  D  /\  B  e.  _V ) )
64, 5mpbiran2 890 . . 3  |-  ( <. A ,  B >.  e.  ( D  X.  _V ) 
<->  A  e.  D )
76anbi2i 678 . 2  |-  ( (
<. A ,  B >.  e.  C  /\  <. A ,  B >.  e.  ( D  X.  _V ) )  <-> 
( <. A ,  B >.  e.  C  /\  A  e.  D ) )
82, 3, 73bitri 264 1  |-  ( <. A ,  B >.  e.  ( C  |`  D )  <-> 
( <. A ,  B >.  e.  C  /\  A  e.  D ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1621   _Vcvv 2757    i^i cin 3112   <.cop 3603    X. cxp 4645    |` cres 4649
This theorem is referenced by:  brres  4935  opelresg  4936  opres  4938  dmres  4950  elres  4964  relssres  4966  resiexg  4971  iss  4972  asymref  5033  ssrnres  5090  cnvresima  5135  ressn  5184  funssres  5218  fcnvres  5342  dprd2dlem1  15224  dprd2da  15225  hausdiag  17287  hauseqlcld  17288  ovoliunlem1  18809  h2hlm  21506  relexpindlem  23394  restidsing  24428  cnvresimaOLD  25579
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-opab 4038  df-xp 4661  df-res 4667
  Copyright terms: Public domain W3C validator