Theorem brel 5731

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3908   class class class wbr 5114   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672

This theorem is used by:  brab2a  5759  soirri  6131  sotri  6132  sotri2  6134  sotri3  6135  ndmovord  7613  ndmovordi  7614  swoer  8735  brecop2  8818  ecopovsym  8826  ecopovtrn  8827  hartogslem1  9514  nlt1pi  10909  indpi  10910  nqerf  10933  ordpipq  10945  lterpq  10973  ltexnq  10978  ltbtwnnq  10981  ltrnq  10982  prnmadd  11000  genpcd  11009  nqpr  11017  1idpr  11032  ltexprlem4  11042  ltexpri  11046  ltaprlem  11047  prlem936  11050  reclem2pr  11051  reclem3pr  11052  reclem4pr  11053  suplem1pr  11055  suplem2pr  11056  supexpr  11057  recexsrlem  11106  addgt0sr  11107  mulgt0sr  11108  mappsrpr  11111  map2psrpr  11113  supsrlem  11114  supsr  11115  ltresr  11143  dfle2  13190  dflt2  13191  dvdszrcl  16340  letsr  18674  hmphtop  23972  brtxp2  36392  brpprod3a  36397  brxrn2  39074  aks6d1c1p1rcl  42916  iccdisj2  49716  i0oii  49739  io1ii  49740