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

Theorem brel 4598
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 3979 . 2  |-  ( A R B  ->  A
( C  X.  D
) B )
3 brxp 4577 . 2  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )
42, 3sylib 121 1  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1481    C_ wss 3075   class class class wbr 3936    X. cxp 4544
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-br 3937  df-opab 3997  df-xp 4552
This theorem is referenced by:  brab2a  4599  brab2ga  4621  soirri  4940  sotri  4941  sotri2  4943  sotri3  4944  swoer  6464  ecopovsym  6532  ecopovtrn  6533  ecopovsymg  6535  ecopovtrng  6536  ltanqi  7233  ltmnqi  7234  ltexnqi  7240  ltbtwnnqq  7246  ltbtwnnq  7247  ltrnqi  7252  prcdnql  7315  prcunqu  7316  prnmaxl  7319  prnminu  7320  prloc  7322  prarloclemcalc  7333  genplt2i  7341  genpcdl  7350  genpcuu  7351  addnqprllem  7358  addnqprulem  7359  addlocprlemlt  7362  addlocprlemeq  7364  addlocprlemgt  7365  addlocprlem  7366  nqprxx  7377  ltnqex  7380  gtnqex  7381  addnqprlemrl  7388  addnqprlemru  7389  addnqprlemfl  7390  addnqprlemfu  7391  appdivnq  7394  prmuloclemcalc  7396  prmuloc  7397  mulnqprlemrl  7404  mulnqprlemru  7405  mulnqprlemfl  7406  mulnqprlemfu  7407  ltprordil  7420  1idprl  7421  1idpru  7422  ltnqpri  7425  ltexprlemm  7431  ltexprlemopl  7432  ltexprlemlol  7433  ltexprlemopu  7434  ltexprlemupu  7435  ltexprlemdisj  7437  ltexprlemloc  7438  ltexprlemfl  7440  ltexprlemrl  7441  ltexprlemfu  7442  ltexprlemru  7443  ltexpri  7444  lteupri  7448  ltaprlem  7449  recexprlemell  7453  recexprlemelu  7454  recexprlemloc  7462  recexprlempr  7463  recexprlem1ssl  7464  recexprlem1ssu  7465  recexprlemss1l  7466  recexprlemss1u  7467  cauappcvgprlemm  7476  cauappcvgprlemlol  7478  cauappcvgprlemupu  7480  cauappcvgprlemladdfu  7485  cauappcvgprlemladdfl  7486  caucvgprlemk  7496  caucvgprlemm  7499  caucvgprlemlol  7501  caucvgprlemupu  7503  caucvgprlemladdfu  7508  caucvgprlem1  7510  caucvgprlem2  7511  caucvgprprlemk  7514  caucvgprprlemloccalc  7515  caucvgprprlemval  7519  caucvgprprlemml  7525  caucvgprprlemlol  7529  caucvgprprlemupu  7531  caucvgprprlemloc  7534  caucvgprprlem1  7540  caucvgprprlem2  7541  suplocexprlemss  7546  suplocexprlemrl  7548  suplocexprlemru  7550  suplocexprlemlub  7555  gt0srpr  7579  recexgt0sr  7604  addgt0sr  7606  mulgt0sr  7609  caucvgsrlemasr  7621  map2psrprg  7636  suplocsrlem  7639  suplocsr  7640  ltresr  7670  ltrenn  7686  dvdszrcl  11532
  Copyright terms: Public domain W3C validator