Theorem brel 5710

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3904   class class class wbr 5099   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651

This theorem is referenced by:  brab2a  5738  soirri  6110  sotri  6111  sotri2  6113  sotri3  6114  ndmovord  7582  ndmovordi  7583  swoer  8705  brecop2  8788  ecopovsym  8796  ecopovtrn  8797  hartogslem1  9487  nlt1pi  10861  indpi  10862  nqerf  10885  ordpipq  10897  lterpq  10925  ltexnq  10930  ltbtwnnq  10933  ltrnq  10934  prnmadd  10952  genpcd  10961  nqpr  10969  1idpr  10984  ltexprlem4  10994  ltexpri  10998  ltaprlem  10999  prlem936  11002  reclem2pr  11003  reclem3pr  11004  reclem4pr  11005  suplem1pr  11007  suplem2pr  11008  supexpr  11009  recexsrlem  11058  addgt0sr  11059  mulgt0sr  11060  mappsrpr  11063  map2psrpr  11065  supsrlem  11066  supsr  11067  ltresr  11095  dfle2  13146  dflt2  13147  dvdszrcl  16274  letsr  18608  hmphtop  23818  brtxp2  36193  brpprod3a  36198  brxrn2  38847  aks6d1c1p1rcl  42689  iccdisj2  49482  i0oii  49505  io1ii  49506