Theorem brel 5689

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901   class class class wbr 5098   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630

This theorem is referenced by:  brab2a  5717  soirri  6083  sotri  6084  sotri2  6086  sotri3  6087  ndmovord  7548  ndmovordi  7549  swoer  8666  brecop2  8748  ecopovsym  8756  ecopovtrn  8757  hartogslem1  9447  nlt1pi  10817  indpi  10818  nqerf  10841  ordpipq  10853  lterpq  10881  ltexnq  10886  ltbtwnnq  10889  ltrnq  10890  prnmadd  10908  genpcd  10917  nqpr  10925  1idpr  10940  ltexprlem4  10950  ltexpri  10954  ltaprlem  10955  prlem936  10958  reclem2pr  10959  reclem3pr  10960  reclem4pr  10961  suplem1pr  10963  suplem2pr  10964  supexpr  10965  recexsrlem  11014  addgt0sr  11015  mulgt0sr  11016  mappsrpr  11019  map2psrpr  11021  supsrlem  11022  supsr  11023  ltresr  11051  dfle2  13061  dflt2  13062  dvdszrcl  16184  letsr  18516  hmphtop  23722  brtxp2  36073  brpprod3a  36078  brxrn2  38565  aks6d1c1p1rcl  42358  iccdisj2  49138  i0oii  49161  io1ii  49162