Theorem relinxp 5799

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

This proof depends on syntax axioms:   ∩ cin 3901   × cxp 5657  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  inxp  5816  elinxp  6016  cnvcnv  6189  tpostpos  8248  brinxper  8730  erinxp  8795  brdom3  10535  brdom5  10536  brdom4  10537  fpwwe2lem7  10650  fpwwe2lem8  10651  fpwwe2lem11  10654  pwsle  17584  opsrtoslem2  22278  cgraer  29264  elrn3  36349  bj-idres  37920  br1cnvinxp  39015  inxprnres  39054  inxpss  39073  inxpss2  39077  iss2  39100  inxp2  39131  inxpxrn  39174