Theorem brel 5681

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3902   class class class wbr 5091   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622

This theorem is referenced by:  brab2a  5709  soirri  6073  sotri  6074  sotri2  6076  sotri3  6077  ndmovord  7536  ndmovordi  7537  swoer  8653  brecop2  8735  ecopovsym  8743  ecopovtrn  8744  hartogslem1  9428  nlt1pi  10794  indpi  10795  nqerf  10818  ordpipq  10830  lterpq  10858  ltexnq  10863  ltbtwnnq  10866  ltrnq  10867  prnmadd  10885  genpcd  10894  nqpr  10902  1idpr  10917  ltexprlem4  10927  ltexpri  10931  ltaprlem  10932  prlem936  10935  reclem2pr  10936  reclem3pr  10937  reclem4pr  10938  suplem1pr  10940  suplem2pr  10941  supexpr  10942  recexsrlem  10991  addgt0sr  10992  mulgt0sr  10993  mappsrpr  10996  map2psrpr  10998  supsrlem  10999  supsr  11000  ltresr  11028  dfle2  13043  dflt2  13044  dvdszrcl  16165  letsr  18496  hmphtop  23691  brtxp2  35914  brpprod3a  35919  brxrn2  38402  aks6d1c1p1rcl  42140  iccdisj2  48927  i0oii  48950  io1ii  48951