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  7608  ndmovordi  7609  swoer  8732  brecop2  8815  ecopovsym  8823  ecopovtrn  8824  hartogslem1  9518  nlt1pi  10919  indpi  10920  nqerf  10943  ordpipq  10955  lterpq  10983  ltexnq  10988  ltbtwnnq  10991  ltrnq  10992  prnmadd  11010  genpcd  11019  nqpr  11027  1idpr  11042  ltexprlem4  11052  ltexpri  11056  ltaprlem  11057  prlem936  11060  reclem2pr  11061  reclem3pr  11062  reclem4pr  11063  suplem1pr  11065  suplem2pr  11066  supexpr  11067  recexsrlem  11116  addgt0sr  11117  mulgt0sr  11118  mappsrpr  11121  map2psrpr  11123  supsrlem  11124  supsr  11125  ltresr  11153  dfle2  13202  dflt2  13203  dvdszrcl  16353  letsr  18687  hmphtop  24010  brtxp2  36466  brpprod3a  36471  brxrn2  39140  aks6d1c1p1rcl  42982  iccdisj2  49831  i0oii  49854  io1ii  49855