Theorem brel 5739

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3947   class class class wbr 5147   × cxp 5673

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 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

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 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681

This theorem is referenced by:  brab2a  5767  soirri  6124  sotri  6125  sotri2  6127  sotri3  6128  ndmovord  7593  ndmovordi  7594  swoer  8729  brecop2  8801  ecopovsym  8809  ecopovtrn  8810  hartogslem1  9533  nlt1pi  10897  indpi  10898  nqerf  10921  ordpipq  10933  lterpq  10961  ltexnq  10966  ltbtwnnq  10969  ltrnq  10970  prnmadd  10988  genpcd  10997  nqpr  11005  1idpr  11020  ltexprlem4  11030  ltexpri  11034  ltaprlem  11035  prlem936  11038  reclem2pr  11039  reclem3pr  11040  reclem4pr  11041  suplem1pr  11043  suplem2pr  11044  supexpr  11045  recexsrlem  11094  addgt0sr  11095  mulgt0sr  11096  mappsrpr  11099  map2psrpr  11101  supsrlem  11102  supsr  11103  ltresr  11131  dfle2  13122  dflt2  13123  dvdszrcl  16198  letsr  18542  hmphtop  23273  brtxp2  34841  brpprod3a  34846  brxrn2  37233  iccdisj2  47483  i0oii  47505  io1ii  47506