Theorem brel 5589

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2113   ⊆ wss 3844   class class class wbr 5031   × cxp 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5168  ax-nul 5175  ax-pr 5297

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3400  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094  df-xp 5532

This theorem is referenced by:  brab2a  5616  soirri  5961  sotri  5962  sotri2  5964  sotri3  5965  ndmovord  7355  ndmovordi  7356  swoer  8351  brecop2  8423  ecopovsym  8431  ecopovtrn  8432  hartogslem1  9080  nlt1pi  10407  indpi  10408  nqerf  10431  ordpipq  10443  lterpq  10471  ltexnq  10476  ltbtwnnq  10479  ltrnq  10480  prnmadd  10498  genpcd  10507  nqpr  10515  1idpr  10530  ltexprlem4  10540  ltexpri  10544  ltaprlem  10545  prlem936  10548  reclem2pr  10549  reclem3pr  10550  reclem4pr  10551  suplem1pr  10553  suplem2pr  10554  supexpr  10555  recexsrlem  10604  addgt0sr  10605  mulgt0sr  10606  mappsrpr  10609  map2psrpr  10611  supsrlem  10612  supsr  10613  ltresr  10641  dfle2  12624  dflt2  12625  dvdszrcl  15705  letsr  17954  hmphtop  22530  brtxp2  33821  brpprod3a  33826  brxrn2  36125  iccdisj2  45706  i0oii  45727  io1ii  45728