Theorem relinxp 5799

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 5677	. 2 ⊢ Rel (𝐴 × 𝐵)
2		relin2 5798	. 2 ⊢ (Rel (𝐴 × 𝐵) → Rel (𝑅 ∩ (𝐴 × 𝐵)))
3	1, 2	ax-mp 5	1 ⊢ Rel (𝑅 ∩ (𝐴 × 𝐵))

Syntax hints:   ∩ cin 3912   × cxp 5657  Rel wrel 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-opab 5175  df-xp 5665  df-rel 5666

This theorem is referenced by:  inxp  5816  elinxp  6016  cnvcnv  6188  tpostpos  8238  brinxper  8720  erinxp  8785  brdom3  10508  brdom5  10509  brdom4  10510  fpwwe2lem7  10618  fpwwe2lem8  10619  fpwwe2lem11  10622  pwsle  17542  opsrtoslem2  22172  elrn3  36149  bj-idres  37687  br1cnvinxp  38793  inxprnres  38832  inxpss  38851  inxpss2  38855  iss2  38878  inxp2  38909  inxpxrn  38952