Theorem brel 4549

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

Step	Hyp	Ref	Expression
1		brel.1	. . 3 |- R C_ ( C X. D )
2	1	ssbri 3935	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4528	. 2 |- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
4	2, 3	sylib 121	1 |- ( A R B -> ( A e. C /\ B e. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1461   C_ wss 3035   class class class wbr 3893   X. cxp 4495

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-br 3894  df-opab 3948  df-xp 4503

This theorem is referenced by:  brab2a  4550  brab2ga  4572  soirri  4889  sotri  4890  sotri2  4892  sotri3  4893  swoer  6409  ecopovsym  6477  ecopovtrn  6478  ecopovsymg  6480  ecopovtrng  6481  ltanqi  7152  ltmnqi  7153  ltexnqi  7159  ltbtwnnqq  7165  ltbtwnnq  7166  ltrnqi  7171  prcdnql  7234  prcunqu  7235  prnmaxl  7238  prnminu  7239  prloc  7241  prarloclemcalc  7252  genplt2i  7260  genpcdl  7269  genpcuu  7270  addnqprllem  7277  addnqprulem  7278  addlocprlemlt  7281  addlocprlemeq  7283  addlocprlemgt  7284  addlocprlem  7285  nqprxx  7296  ltnqex  7299  gtnqex  7300  addnqprlemrl  7307  addnqprlemru  7308  addnqprlemfl  7309  addnqprlemfu  7310  appdivnq  7313  prmuloclemcalc  7315  prmuloc  7316  mulnqprlemrl  7323  mulnqprlemru  7324  mulnqprlemfl  7325  mulnqprlemfu  7326  ltprordil  7339  1idprl  7340  1idpru  7341  ltnqpri  7344  ltexprlemm  7350  ltexprlemopl  7351  ltexprlemlol  7352  ltexprlemopu  7353  ltexprlemupu  7354  ltexprlemdisj  7356  ltexprlemloc  7357  ltexprlemfl  7359  ltexprlemrl  7360  ltexprlemfu  7361  ltexprlemru  7362  ltexpri  7363  lteupri  7367  ltaprlem  7368  recexprlemell  7372  recexprlemelu  7373  recexprlemloc  7381  recexprlempr  7382  recexprlem1ssl  7383  recexprlem1ssu  7384  recexprlemss1l  7385  recexprlemss1u  7386  cauappcvgprlemm  7395  cauappcvgprlemlol  7397  cauappcvgprlemupu  7399  cauappcvgprlemladdfu  7404  cauappcvgprlemladdfl  7405  caucvgprlemk  7415  caucvgprlemm  7418  caucvgprlemlol  7420  caucvgprlemupu  7422  caucvgprlemladdfu  7427  caucvgprlem1  7429  caucvgprlem2  7430  caucvgprprlemk  7433  caucvgprprlemloccalc  7434  caucvgprprlemval  7438  caucvgprprlemml  7444  caucvgprprlemlol  7448  caucvgprprlemupu  7450  caucvgprprlemloc  7453  caucvgprprlem1  7459  caucvgprprlem2  7460  gt0srpr  7485  recexgt0sr  7510  addgt0sr  7512  mulgt0sr  7514  caucvgsrlemasr  7526  ltresr  7568  ltrenn  7584  dvdszrcl  11340