Theorem relinxp 5827

Description: Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.)

Assertion

Ref	Expression
relinxp	⊢ Rel (𝑅 ∩ (𝐴 × 𝐵))

Proof of Theorem relinxp

Step	Hyp	Ref	Expression
1		relxp 5707	. 2 ⊢ Rel (𝐴 × 𝐵)
2		relin2 5826	. 2 ⊢ (Rel (𝐴 × 𝐵) → Rel (𝑅 ∩ (𝐴 × 𝐵)))
3	1, 2	ax-mp 5	1 ⊢ Rel (𝑅 ∩ (𝐴 × 𝐵))

Syntax hints:   ∩ cin 3962   × cxp 5687  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-opab 5211  df-xp 5695  df-rel 5696

This theorem is referenced by:  inxp  5845  elinxp  6039  cnvcnv  6214  tpostpos  8270  brinxper  8773  erinxp  8830  brdom3  10566  brdom5  10567  brdom4  10568  fpwwe2lem7  10675  fpwwe2lem8  10676  fpwwe2lem11  10679  pwsle  17539  opsrtoslem2  22098  elrn3  35742  bj-idres  37143  br1cnvinxp  38238  inxprnres  38274  inxpss  38293  inxpss2  38297  iss2  38326  inxp2  38349  inxpxrn  38377