Theorem brel 4672

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	⊢ 𝑅 ⊆ (𝐶 × 𝐷)

Assertion

Ref	Expression
brel	⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem brel

Step	Hyp	Ref	Expression
1		brel.1	. . 3 ⊢ 𝑅 ⊆ (𝐶 × 𝐷)
2	1	ssbri 4042	. 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵)
3		brxp 4651	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
4	2, 3	sylib 122	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2146   ⊆ wss 3127   class class class wbr 3998   × cxp 4618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-opab 4060  df-xp 4626

This theorem is referenced by:  brab2a  4673  brab2ga  4695  soirri  5015  sotri  5016  sotri2  5018  sotri3  5019  swoer  6553  ecopovsym  6621  ecopovtrn  6622  ecopovsymg  6624  ecopovtrng  6625  ltanqi  7376  ltmnqi  7377  ltexnqi  7383  ltbtwnnqq  7389  ltbtwnnq  7390  ltrnqi  7395  prcdnql  7458  prcunqu  7459  prnmaxl  7462  prnminu  7463  prloc  7465  prarloclemcalc  7476  genplt2i  7484  genpcdl  7493  genpcuu  7494  addnqprllem  7501  addnqprulem  7502  addlocprlemlt  7505  addlocprlemeq  7507  addlocprlemgt  7508  addlocprlem  7509  nqprxx  7520  ltnqex  7523  gtnqex  7524  addnqprlemrl  7531  addnqprlemru  7532  addnqprlemfl  7533  addnqprlemfu  7534  appdivnq  7537  prmuloclemcalc  7539  prmuloc  7540  mulnqprlemrl  7547  mulnqprlemru  7548  mulnqprlemfl  7549  mulnqprlemfu  7550  ltprordil  7563  1idprl  7564  1idpru  7565  ltnqpri  7568  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemlol  7576  ltexprlemopu  7577  ltexprlemupu  7578  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  ltexpri  7587  lteupri  7591  ltaprlem  7592  recexprlemell  7596  recexprlemelu  7597  recexprlemloc  7605  recexprlempr  7606  recexprlem1ssl  7607  recexprlem1ssu  7608  recexprlemss1l  7609  recexprlemss1u  7610  cauappcvgprlemm  7619  cauappcvgprlemlol  7621  cauappcvgprlemupu  7623  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  caucvgprlemk  7639  caucvgprlemm  7642  caucvgprlemlol  7644  caucvgprlemupu  7646  caucvgprlemladdfu  7651  caucvgprlem1  7653  caucvgprlem2  7654  caucvgprprlemk  7657  caucvgprprlemloccalc  7658  caucvgprprlemval  7662  caucvgprprlemml  7668  caucvgprprlemlol  7672  caucvgprprlemupu  7674  caucvgprprlemloc  7677  caucvgprprlem1  7683  caucvgprprlem2  7684  suplocexprlemss  7689  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemlub  7698  gt0srpr  7722  recexgt0sr  7747  addgt0sr  7749  mulgt0sr  7752  caucvgsrlemasr  7764  map2psrprg  7779  suplocsrlem  7782  suplocsr  7783  ltresr  7813  ltrenn  7829  dvdszrcl  11765