Theorem brel 5653

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   ⊆ wss 3888   class class class wbr 5075   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596

This theorem is referenced by:  brab2a  5681  soirri  6036  sotri  6037  sotri2  6039  sotri3  6040  ndmovord  7471  ndmovordi  7472  swoer  8537  brecop2  8609  ecopovsym  8617  ecopovtrn  8618  hartogslem1  9310  nlt1pi  10671  indpi  10672  nqerf  10695  ordpipq  10707  lterpq  10735  ltexnq  10740  ltbtwnnq  10743  ltrnq  10744  prnmadd  10762  genpcd  10771  nqpr  10779  1idpr  10794  ltexprlem4  10804  ltexpri  10808  ltaprlem  10809  prlem936  10812  reclem2pr  10813  reclem3pr  10814  reclem4pr  10815  suplem1pr  10817  suplem2pr  10818  supexpr  10819  recexsrlem  10868  addgt0sr  10869  mulgt0sr  10870  mappsrpr  10873  map2psrpr  10875  supsrlem  10876  supsr  10877  ltresr  10905  dfle2  12890  dflt2  12891  dvdszrcl  15977  letsr  18320  hmphtop  22938  brtxp2  34192  brpprod3a  34197  brxrn2  36512  iccdisj2  46202  i0oii  46224  io1ii  46225