Theorem brel 4900

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	|- R C_ ( C X. D )

Assertion

Ref	Expression
brel	|- ( A R B -> ( A e. C /\ B e. D ) )

Proof of Theorem brel

Step	Hyp	Ref	Expression
1		brel.1	. . 3 |- R C_ ( C X. D )
2	1	ssbri 4464	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4882	. 2 |- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
4	2, 3	sylib 200	1 |- ( A R B -> ( A e. C /\ B e. D ) )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1869   C_ wss 3437   class class class wbr 4421   X. cxp 4849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-xp 4857

This theorem is referenced by:  brab2a  4901  brab2ga  4927  soirri  5243  sotri  5244  sotri2  5246  sotri3  5247  ndmovord  6471  ndmovordi  6472  swoer  7397  brecop2  7463  ecopovsym  7471  ecopovtrn  7472  hartogslem1  8061  nlt1pi  9333  indpi  9334  nqerf  9357  ordpipq  9369  lterpq  9397  ltexnq  9402  ltbtwnnq  9405  ltrnq  9406  prnmadd  9424  genpcd  9433  nqpr  9441  1idpr  9456  ltexprlem4  9466  ltexpri  9470  ltaprlem  9471  prlem936  9474  reclem2pr  9475  reclem3pr  9476  reclem4pr  9477  suplem1pr  9479  suplem2pr  9480  supexpr  9481  recexsrlem  9529  addgt0sr  9530  mulgt0sr  9531  mappsrpr  9534  map2psrpr  9536  supsrlem  9537  supsr  9538  ltresr  9566  dfle2  11448  dflt2  11449  dvdszrcl  14303  letsr  16466  hmphtop  20785  vcex  26191  brtxp2  30647  brpprod3a  30652