Theorem relinxp 5824

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

Syntax hints:   ∩ cin 3950   × cxp 5683  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  inxp  5842  elinxp  6037  cnvcnv  6212  tpostpos  8271  brinxper  8774  erinxp  8831  brdom3  10568  brdom5  10569  brdom4  10570  fpwwe2lem7  10677  fpwwe2lem8  10678  fpwwe2lem11  10681  pwsle  17537  opsrtoslem2  22080  elrn3  35762  bj-idres  37161  br1cnvinxp  38257  inxprnres  38293  inxpss  38312  inxpss2  38316  iss2  38345  inxp2  38368  inxpxrn  38396