Theorem brel 5765

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976   class class class wbr 5166   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706

This theorem is referenced by:  brab2a  5793  soirri  6158  sotri  6159  sotri2  6161  sotri3  6162  ndmovord  7640  ndmovordi  7641  swoer  8794  brecop2  8869  ecopovsym  8877  ecopovtrn  8878  hartogslem1  9611  nlt1pi  10975  indpi  10976  nqerf  10999  ordpipq  11011  lterpq  11039  ltexnq  11044  ltbtwnnq  11047  ltrnq  11048  prnmadd  11066  genpcd  11075  nqpr  11083  1idpr  11098  ltexprlem4  11108  ltexpri  11112  ltaprlem  11113  prlem936  11116  reclem2pr  11117  reclem3pr  11118  reclem4pr  11119  suplem1pr  11121  suplem2pr  11122  supexpr  11123  recexsrlem  11172  addgt0sr  11173  mulgt0sr  11174  mappsrpr  11177  map2psrpr  11179  supsrlem  11180  supsr  11181  ltresr  11209  dfle2  13209  dflt2  13210  dvdszrcl  16307  letsr  18663  hmphtop  23807  brtxp2  35845  brpprod3a  35850  brxrn2  38331  aks6d1c1p1rcl  42065  iccdisj2  48577  i0oii  48599  io1ii  48600