Theorem brel 5733

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3944   class class class wbr 5141   × cxp 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-xp 5675

This theorem is referenced by:  brab2a  5761  soirri  6116  sotri  6117  sotri2  6119  sotri3  6120  ndmovord  7580  ndmovordi  7581  swoer  8716  brecop2  8788  ecopovsym  8796  ecopovtrn  8797  hartogslem1  9519  nlt1pi  10883  indpi  10884  nqerf  10907  ordpipq  10919  lterpq  10947  ltexnq  10952  ltbtwnnq  10955  ltrnq  10956  prnmadd  10974  genpcd  10983  nqpr  10991  1idpr  11006  ltexprlem4  11016  ltexpri  11020  ltaprlem  11021  prlem936  11024  reclem2pr  11025  reclem3pr  11026  reclem4pr  11027  suplem1pr  11029  suplem2pr  11030  supexpr  11031  recexsrlem  11080  addgt0sr  11081  mulgt0sr  11082  mappsrpr  11085  map2psrpr  11087  supsrlem  11088  supsr  11089  ltresr  11117  dfle2  13108  dflt2  13109  dvdszrcl  16184  letsr  18528  hmphtop  23211  brtxp2  34683  brpprod3a  34688  brxrn2  37050  iccdisj2  47178  i0oii  47200  io1ii  47201