Theorem brel 5749

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   ⊆ wss 3950   class class class wbr 5142   × cxp 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690

This theorem is referenced by:  brab2a  5778  soirri  6145  sotri  6146  sotri2  6148  sotri3  6149  ndmovord  7624  ndmovordi  7625  swoer  8777  brecop2  8852  ecopovsym  8860  ecopovtrn  8861  hartogslem1  9583  nlt1pi  10947  indpi  10948  nqerf  10971  ordpipq  10983  lterpq  11011  ltexnq  11016  ltbtwnnq  11019  ltrnq  11020  prnmadd  11038  genpcd  11047  nqpr  11055  1idpr  11070  ltexprlem4  11080  ltexpri  11084  ltaprlem  11085  prlem936  11088  reclem2pr  11089  reclem3pr  11090  reclem4pr  11091  suplem1pr  11093  suplem2pr  11094  supexpr  11095  recexsrlem  11144  addgt0sr  11145  mulgt0sr  11146  mappsrpr  11149  map2psrpr  11151  supsrlem  11152  supsr  11153  ltresr  11181  dfle2  13190  dflt2  13191  dvdszrcl  16296  letsr  18639  hmphtop  23787  brtxp2  35883  brpprod3a  35888  brxrn2  38377  aks6d1c1p1rcl  42110  iccdisj2  48801  i0oii  48824  io1ii  48825