Theorem brel 4591

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 3972	. 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵)
3		brxp 4570	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
4	2, 3	sylib 121	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480   ⊆ wss 3071   class class class wbr 3929   × cxp 4537

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930  df-opab 3990  df-xp 4545

This theorem is referenced by:  brab2a  4592  brab2ga  4614  soirri  4933  sotri  4934  sotri2  4936  sotri3  4937  swoer  6457  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  ltanqi  7210  ltmnqi  7211  ltexnqi  7217  ltbtwnnqq  7223  ltbtwnnq  7224  ltrnqi  7229  prcdnql  7292  prcunqu  7293  prnmaxl  7296  prnminu  7297  prloc  7299  prarloclemcalc  7310  genplt2i  7318  genpcdl  7327  genpcuu  7328  addnqprllem  7335  addnqprulem  7336  addlocprlemlt  7339  addlocprlemeq  7341  addlocprlemgt  7342  addlocprlem  7343  nqprxx  7354  ltnqex  7357  gtnqex  7358  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  appdivnq  7371  prmuloclemcalc  7373  prmuloc  7374  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  ltprordil  7397  1idprl  7398  1idpru  7399  ltnqpri  7402  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  ltexpri  7421  lteupri  7425  ltaprlem  7426  recexprlemell  7430  recexprlemelu  7431  recexprlemloc  7439  recexprlempr  7440  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemm  7453  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemk  7473  caucvgprlemm  7476  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprlemladdfu  7485  caucvgprlem1  7487  caucvgprlem2  7488  caucvgprprlemk  7491  caucvgprprlemloccalc  7492  caucvgprprlemval  7496  caucvgprprlemml  7502  caucvgprprlemlol  7506  caucvgprprlemupu  7508  caucvgprprlemloc  7511  caucvgprprlem1  7517  caucvgprprlem2  7518  suplocexprlemss  7523  suplocexprlemrl  7525  suplocexprlemru  7527  suplocexprlemlub  7532  gt0srpr  7556  recexgt0sr  7581  addgt0sr  7583  mulgt0sr  7586  caucvgsrlemasr  7598  map2psrprg  7613  suplocsrlem  7616  suplocsr  7617  ltresr  7647  ltrenn  7663  dvdszrcl  11498