Theorem relinxp 5761

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

Syntax hints:   ∩ cin 3904   × cxp 5621  Rel wrel 5628

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  inxp  5778  elinxp  5974  cnvcnv  6145  tpostpos  8186  brinxper  8661  erinxp  8725  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem7  10550  fpwwe2lem8  10551  fpwwe2lem11  10554  pwsle  17414  opsrtoslem2  21979  elrn3  35734  bj-idres  37133  br1cnvinxp  38230  inxprnres  38265  inxpss  38284  inxpss2  38288  iss2  38311  inxp2  38334  inxpxrn  38366