Theorem brel 5742

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3949   class class class wbr 5149   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683

This theorem is referenced by:  brab2a  5770  soirri  6128  sotri  6129  sotri2  6131  sotri3  6132  ndmovord  7597  ndmovordi  7598  swoer  8733  brecop2  8805  ecopovsym  8813  ecopovtrn  8814  hartogslem1  9537  nlt1pi  10901  indpi  10902  nqerf  10925  ordpipq  10937  lterpq  10965  ltexnq  10970  ltbtwnnq  10973  ltrnq  10974  prnmadd  10992  genpcd  11001  nqpr  11009  1idpr  11024  ltexprlem4  11034  ltexpri  11038  ltaprlem  11039  prlem936  11042  reclem2pr  11043  reclem3pr  11044  reclem4pr  11045  suplem1pr  11047  suplem2pr  11048  supexpr  11049  recexsrlem  11098  addgt0sr  11099  mulgt0sr  11100  mappsrpr  11103  map2psrpr  11105  supsrlem  11106  supsr  11107  ltresr  11135  dfle2  13126  dflt2  13127  dvdszrcl  16202  letsr  18546  hmphtop  23282  brtxp2  34853  brpprod3a  34858  brxrn2  37245  iccdisj2  47530  i0oii  47552  io1ii  47553