Theorem brel 5728

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906   class class class wbr 5110   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669

This theorem is referenced by:  brab2a  5756  soirri  6128  sotri  6129  sotri2  6131  sotri3  6132  ndmovord  7602  ndmovordi  7603  swoer  8727  brecop2  8810  ecopovsym  8818  ecopovtrn  8819  hartogslem1  9505  nlt1pi  10892  indpi  10893  nqerf  10916  ordpipq  10928  lterpq  10956  ltexnq  10961  ltbtwnnq  10964  ltrnq  10965  prnmadd  10983  genpcd  10992  nqpr  11000  1idpr  11015  ltexprlem4  11025  ltexpri  11029  ltaprlem  11030  prlem936  11033  reclem2pr  11034  reclem3pr  11035  reclem4pr  11036  suplem1pr  11038  suplem2pr  11039  supexpr  11040  recexsrlem  11089  addgt0sr  11090  mulgt0sr  11091  mappsrpr  11094  map2psrpr  11096  supsrlem  11097  supsr  11098  ltresr  11126  dfle2  13173  dflt2  13174  dvdszrcl  16316  letsr  18650  hmphtop  23916  brtxp2  36349  brpprod3a  36354  brxrn2  39011  aks6d1c1p1rcl  42853  iccdisj2  49652  i0oii  49675  io1ii  49676