Theorem relinxp 5771

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

Syntax hints:   ∩ cin 3902   × cxp 5630  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  inxp  5788  elinxp  5986  cnvcnv  6158  tpostpos  8198  brinxper  8675  erinxp  8740  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem7  10560  fpwwe2lem8  10561  fpwwe2lem11  10564  pwsle  17425  opsrtoslem2  22023  elrn3  35975  bj-idres  37409  br1cnvinxp  38504  inxprnres  38543  inxpss  38562  inxpss2  38566  iss2  38589  inxp2  38620  inxpxrn  38663