Theorem relinxp 5754

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

Syntax hints:   ∩ cin 3901   × cxp 5614  Rel wrel 5621

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3909  df-ss 3919  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  inxp  5771  elinxp  5968  cnvcnv  6139  tpostpos  8176  brinxper  8651  erinxp  8715  brdom3  10419  brdom5  10420  brdom4  10421  fpwwe2lem7  10528  fpwwe2lem8  10529  fpwwe2lem11  10532  pwsle  17396  opsrtoslem2  21992  elrn3  35804  bj-idres  37200  br1cnvinxp  38297  inxprnres  38332  inxpss  38351  inxpss2  38355  iss2  38378  inxp2  38401  inxpxrn  38433