Theorem brel 5703

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914   class class class wbr 5107   × cxp 5636

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644

This theorem is referenced by:  brab2a  5732  soirri  6099  sotri  6100  sotri2  6102  sotri3  6103  ndmovord  7579  ndmovordi  7580  swoer  8702  brecop2  8784  ecopovsym  8792  ecopovtrn  8793  hartogslem1  9495  nlt1pi  10859  indpi  10860  nqerf  10883  ordpipq  10895  lterpq  10923  ltexnq  10928  ltbtwnnq  10931  ltrnq  10932  prnmadd  10950  genpcd  10959  nqpr  10967  1idpr  10982  ltexprlem4  10992  ltexpri  10996  ltaprlem  10997  prlem936  11000  reclem2pr  11001  reclem3pr  11002  reclem4pr  11003  suplem1pr  11005  suplem2pr  11006  supexpr  11007  recexsrlem  11056  addgt0sr  11057  mulgt0sr  11058  mappsrpr  11061  map2psrpr  11063  supsrlem  11064  supsr  11065  ltresr  11093  dfle2  13107  dflt2  13108  dvdszrcl  16227  letsr  18552  hmphtop  23665  brtxp2  35869  brpprod3a  35874  brxrn2  38357  aks6d1c1p1rcl  42096  iccdisj2  48885  i0oii  48908  io1ii  48909