Theorem relinxp 5758

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

Syntax hints:   ∩ cin 3897   × cxp 5617  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915  df-opab 5156  df-xp 5625  df-rel 5626

This theorem is referenced by:  inxp  5775  elinxp  5972  cnvcnv  6144  tpostpos  8182  brinxper  8657  erinxp  8721  brdom3  10426  brdom5  10427  brdom4  10428  fpwwe2lem7  10535  fpwwe2lem8  10536  fpwwe2lem11  10539  pwsle  17398  opsrtoslem2  21992  elrn3  35827  bj-idres  37225  br1cnvinxp  38314  inxprnres  38351  inxpss  38370  inxpss2  38374  iss2  38397  inxp2  38420  inxpxrn  38463