Theorem brel 5706

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3917   class class class wbr 5110   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647

This theorem is referenced by:  brab2a  5735  soirri  6102  sotri  6103  sotri2  6105  sotri3  6106  ndmovord  7582  ndmovordi  7583  swoer  8705  brecop2  8787  ecopovsym  8795  ecopovtrn  8796  hartogslem1  9502  nlt1pi  10866  indpi  10867  nqerf  10890  ordpipq  10902  lterpq  10930  ltexnq  10935  ltbtwnnq  10938  ltrnq  10939  prnmadd  10957  genpcd  10966  nqpr  10974  1idpr  10989  ltexprlem4  10999  ltexpri  11003  ltaprlem  11004  prlem936  11007  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010  suplem1pr  11012  suplem2pr  11013  supexpr  11014  recexsrlem  11063  addgt0sr  11064  mulgt0sr  11065  mappsrpr  11068  map2psrpr  11070  supsrlem  11071  supsr  11072  ltresr  11100  dfle2  13114  dflt2  13115  dvdszrcl  16234  letsr  18559  hmphtop  23672  brtxp2  35876  brpprod3a  35881  brxrn2  38364  aks6d1c1p1rcl  42103  iccdisj2  48889  i0oii  48912  io1ii  48913