Theorem relinxp 5793

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

Syntax hints:   ∩ cin 3925   × cxp 5652  Rel wrel 5659

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  inxp  5811  elinxp  6006  cnvcnv  6181  tpostpos  8245  brinxper  8748  erinxp  8805  brdom3  10542  brdom5  10543  brdom4  10544  fpwwe2lem7  10651  fpwwe2lem8  10652  fpwwe2lem11  10655  pwsle  17506  opsrtoslem2  22014  elrn3  35779  bj-idres  37178  br1cnvinxp  38274  inxprnres  38310  inxpss  38329  inxpss2  38333  iss2  38362  inxp2  38385  inxpxrn  38413