Theorem relinxp 5770

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

Syntax hints:   ∩ cin 3888   × cxp 5629  Rel wrel 5636

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  inxp  5787  elinxp  5984  cnvcnv  6156  tpostpos  8196  brinxper  8673  erinxp  8738  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem7  10560  fpwwe2lem8  10561  fpwwe2lem11  10564  pwsle  17456  opsrtoslem2  22034  elrn3  35944  bj-idres  37474  br1cnvinxp  38580  inxprnres  38619  inxpss  38638  inxpss2  38642  iss2  38665  inxp2  38696  inxpxrn  38739