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

Theorem brel 4886
Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypothesis
Ref Expression
brel.1  |-  R  C_  ( C  X.  D
)
Assertion
Ref Expression
brel  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)

Proof of Theorem brel
StepHypRef Expression
1 brel.1 . . 3  |-  R  C_  ( C  X.  D
)
21ssbri 4448 . 2  |-  ( A R B  ->  A
( C  X.  D
) B )
3 brxp 4868 . 2  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )
42, 3sylib 200 1  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1889    C_ wss 3406   class class class wbr 4405    X. cxp 4835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-xp 4843
This theorem is referenced by:  brab2a  4887  brab2ga  4913  soirri  5229  sotri  5230  sotri2  5232  sotri3  5233  ndmovord  6464  ndmovordi  6465  swoer  7396  brecop2  7462  ecopovsym  7470  ecopovtrn  7471  hartogslem1  8062  nlt1pi  9336  indpi  9337  nqerf  9360  ordpipq  9372  lterpq  9400  ltexnq  9405  ltbtwnnq  9408  ltrnq  9409  prnmadd  9427  genpcd  9436  nqpr  9444  1idpr  9459  ltexprlem4  9469  ltexpri  9473  ltaprlem  9474  prlem936  9477  reclem2pr  9478  reclem3pr  9479  reclem4pr  9480  suplem1pr  9482  suplem2pr  9483  supexpr  9484  recexsrlem  9532  addgt0sr  9533  mulgt0sr  9534  mappsrpr  9537  map2psrpr  9539  supsrlem  9540  supsr  9541  ltresr  9569  dfle2  11453  dflt2  11454  dvdszrcl  14322  letsr  16485  hmphtop  20805  vcex  26211  brtxp2  30660  brpprod3a  30665
  Copyright terms: Public domain W3C validator