Theorem relinxp 5792

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

Syntax hints:   ∩ cin 3906   × cxp 5650  Rel wrel 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-in 3914  df-ss 3924  df-opab 5168  df-xp 5658  df-rel 5659

This theorem is referenced by:  inxp  5809  elinxp  6009  cnvcnv  6182  tpostpos  8230  brinxper  8712  erinxp  8777  brdom3  10500  brdom5  10501  brdom4  10502  fpwwe2lem7  10610  fpwwe2lem8  10611  fpwwe2lem11  10614  pwsle  17536  opsrtoslem2  22167  elrn3  36125  bj-idres  37664  br1cnvinxp  38770  inxprnres  38809  inxpss  38828  inxpss2  38832  iss2  38855  inxp2  38886  inxpxrn  38929