Theorem brel 5716

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3899   class class class wbr 5103   × cxp 5649

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657

This theorem is used by:  brab2a  5744  soirri  6118  sotri  6119  sotri2  6121  sotri3  6122  ndmovord  7603  ndmovordi  7604  swoer  8733  brecop2  8816  ecopovsym  8824  ecopovtrn  8825  hartogslem1  9520  nlt1pi  10972  indpi  10973  nqerf  10996  ordpipq  11008  lterpq  11036  ltexnq  11041  ltbtwnnq  11044  ltrnq  11045  prnmadd  11063  genpcd  11072  nqpr  11080  1idpr  11095  ltexprlem4  11105  ltexpri  11109  ltaprlem  11110  prlem936  11113  reclem2pr  11114  reclem3pr  11115  reclem4pr  11116  suplem1pr  11118  suplem2pr  11119  supexpr  11120  recexsrlem  11169  addgt0sr  11170  mulgt0sr  11171  mappsrpr  11174  map2psrpr  11176  supsrlem  11177  supsr  11178  ltresr  11206  dfle2  13257  dflt2  13258  dvdszrcl  16407  letsr  18747  hmphtop  24077  brtxp2  36613  brpprod3a  36618  brxrn2  39284  aks6d1c1p1rcl  43126  iccdisj2  49949  i0oii  49972  io1ii  49973