Theorem brel 5724

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3902   class class class wbr 5107   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665

This theorem is used by:  brab2a  5752  soirri  6124  sotri  6125  sotri2  6127  sotri3  6128  ndmovord  7607  ndmovordi  7608  swoer  8731  brecop2  8814  ecopovsym  8822  ecopovtrn  8823  hartogslem1  9517  nlt1pi  10918  indpi  10919  nqerf  10942  ordpipq  10954  lterpq  10982  ltexnq  10987  ltbtwnnq  10990  ltrnq  10991  prnmadd  11009  genpcd  11018  nqpr  11026  1idpr  11041  ltexprlem4  11051  ltexpri  11055  ltaprlem  11056  prlem936  11059  reclem2pr  11060  reclem3pr  11061  reclem4pr  11062  suplem1pr  11064  suplem2pr  11065  supexpr  11066  recexsrlem  11115  addgt0sr  11116  mulgt0sr  11117  mappsrpr  11120  map2psrpr  11122  supsrlem  11123  supsr  11124  ltresr  11152  dfle2  13200  dflt2  13201  dvdszrcl  16351  letsr  18685  hmphtop  24005  brtxp2  36445  brpprod3a  36450  brxrn2  39119  aks6d1c1p1rcl  42961  iccdisj2  49810  i0oii  49833  io1ii  49834