Theorem brel 5690

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3890   class class class wbr 5079   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631

This theorem is referenced by:  brab2a  5718  soirri  6083  sotri  6084  sotri2  6086  sotri3  6087  ndmovord  7553  ndmovordi  7554  swoer  8672  brecop2  8755  ecopovsym  8763  ecopovtrn  8764  hartogslem1  9454  nlt1pi  10827  indpi  10828  nqerf  10851  ordpipq  10863  lterpq  10891  ltexnq  10896  ltbtwnnq  10899  ltrnq  10900  prnmadd  10918  genpcd  10927  nqpr  10935  1idpr  10950  ltexprlem4  10960  ltexpri  10964  ltaprlem  10965  prlem936  10968  reclem2pr  10969  reclem3pr  10970  reclem4pr  10971  suplem1pr  10973  suplem2pr  10974  supexpr  10975  recexsrlem  11024  addgt0sr  11025  mulgt0sr  11026  mappsrpr  11029  map2psrpr  11031  supsrlem  11032  supsr  11033  ltresr  11061  dfle2  13096  dflt2  13097  dvdszrcl  16224  letsr  18557  hmphtop  23768  brtxp2  36114  brpprod3a  36119  brxrn2  38758  aks6d1c1p1rcl  42600  iccdisj2  49394  i0oii  49417  io1ii  49418