Theorem brel 4711

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164   ⊆ wss 3153   class class class wbr 4029   × cxp 4657

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030  df-opab 4091  df-xp 4665

This theorem is referenced by:  brab2a  4712  brab2ga  4734  soirri  5060  sotri  5061  sotri2  5063  sotri3  5064  swoer  6615  ecopovsym  6685  ecopovtrn  6686  ecopovsymg  6688  ecopovtrng  6689  ltanqi  7462  ltmnqi  7463  ltexnqi  7469  ltbtwnnqq  7475  ltbtwnnq  7476  ltrnqi  7481  prcdnql  7544  prcunqu  7545  prnmaxl  7548  prnminu  7549  prloc  7551  prarloclemcalc  7562  genplt2i  7570  genpcdl  7579  genpcuu  7580  addnqprllem  7587  addnqprulem  7588  addlocprlemlt  7591  addlocprlemeq  7593  addlocprlemgt  7594  addlocprlem  7595  nqprxx  7606  ltnqex  7609  gtnqex  7610  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  appdivnq  7623  prmuloclemcalc  7625  prmuloc  7626  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  ltprordil  7649  1idprl  7650  1idpru  7651  ltnqpri  7654  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  ltexpri  7673  lteupri  7677  ltaprlem  7678  recexprlemell  7682  recexprlemelu  7683  recexprlemloc  7691  recexprlempr  7692  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemm  7705  cauappcvgprlemlol  7707  cauappcvgprlemupu  7709  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemk  7725  caucvgprlemm  7728  caucvgprlemlol  7730  caucvgprlemupu  7732  caucvgprlemladdfu  7737  caucvgprlem1  7739  caucvgprlem2  7740  caucvgprprlemk  7743  caucvgprprlemloccalc  7744  caucvgprprlemval  7748  caucvgprprlemml  7754  caucvgprprlemlol  7758  caucvgprprlemupu  7760  caucvgprprlemloc  7763  caucvgprprlem1  7769  caucvgprprlem2  7770  suplocexprlemss  7775  suplocexprlemrl  7777  suplocexprlemru  7779  suplocexprlemlub  7784  gt0srpr  7808  recexgt0sr  7833  addgt0sr  7835  mulgt0sr  7838  caucvgsrlemasr  7850  map2psrprg  7865  suplocsrlem  7868  suplocsr  7869  ltresr  7899  ltrenn  7915  dvdszrcl  11935