Theorem relinxp 5763

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

Syntax hints:   ∩ cin 3889   × cxp 5622  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  inxp  5780  elinxp  5978  cnvcnv  6150  tpostpos  8189  brinxper  8666  erinxp  8731  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem7  10551  fpwwe2lem8  10552  fpwwe2lem11  10555  pwsle  17447  opsrtoslem2  22044  elrn3  35960  bj-idres  37490  br1cnvinxp  38594  inxprnres  38633  inxpss  38652  inxpss2  38656  iss2  38679  inxp2  38710  inxpxrn  38753