Theorem brel 5688

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3905   class class class wbr 5095   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629

This theorem is referenced by:  brab2a  5716  soirri  6079  sotri  6080  sotri2  6082  sotri3  6083  ndmovord  7543  ndmovordi  7544  swoer  8663  brecop2  8745  ecopovsym  8753  ecopovtrn  8754  hartogslem1  9453  nlt1pi  10819  indpi  10820  nqerf  10843  ordpipq  10855  lterpq  10883  ltexnq  10888  ltbtwnnq  10891  ltrnq  10892  prnmadd  10910  genpcd  10919  nqpr  10927  1idpr  10942  ltexprlem4  10952  ltexpri  10956  ltaprlem  10957  prlem936  10960  reclem2pr  10961  reclem3pr  10962  reclem4pr  10963  suplem1pr  10965  suplem2pr  10966  supexpr  10967  recexsrlem  11016  addgt0sr  11017  mulgt0sr  11018  mappsrpr  11021  map2psrpr  11023  supsrlem  11024  supsr  11025  ltresr  11053  dfle2  13067  dflt2  13068  dvdszrcl  16186  letsr  18517  hmphtop  23681  brtxp2  35854  brpprod3a  35859  brxrn2  38342  aks6d1c1p1rcl  42081  iccdisj2  48882  i0oii  48905  io1ii  48906