Theorem brel 5717

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   ⊆ wss 3907   class class class wbr 5105   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658

This theorem is referenced by:  brab2a  5745  soirri  6117  sotri  6118  sotri2  6120  sotri3  6121  ndmovord  7590  ndmovordi  7591  swoer  8714  brecop2  8797  ecopovsym  8805  ecopovtrn  8806  hartogslem1  9492  nlt1pi  10879  indpi  10880  nqerf  10903  ordpipq  10915  lterpq  10943  ltexnq  10948  ltbtwnnq  10951  ltrnq  10952  prnmadd  10970  genpcd  10979  nqpr  10987  1idpr  11002  ltexprlem4  11012  ltexpri  11016  ltaprlem  11017  prlem936  11020  reclem2pr  11021  reclem3pr  11022  reclem4pr  11023  suplem1pr  11025  suplem2pr  11026  supexpr  11027  recexsrlem  11076  addgt0sr  11077  mulgt0sr  11078  mappsrpr  11081  map2psrpr  11083  supsrlem  11084  supsr  11085  ltresr  11113  dfle2  13163  dflt2  13164  dvdszrcl  16305  letsr  18639  hmphtop  23896  brtxp2  36242  brpprod3a  36247  brxrn2  38895  aks6d1c1p1rcl  42737  iccdisj2  49526  i0oii  49549  io1ii  49550