Theorem relinxp 5777

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

Syntax hints:   ∩ cin 3913   × cxp 5636  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  inxp  5795  elinxp  5990  cnvcnv  6165  tpostpos  8225  brinxper  8700  erinxp  8764  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe2lem7  10590  fpwwe2lem8  10591  fpwwe2lem11  10594  pwsle  17455  opsrtoslem2  21963  elrn3  35749  bj-idres  37148  br1cnvinxp  38245  inxprnres  38280  inxpss  38299  inxpss2  38303  iss2  38326  inxp2  38349  inxpxrn  38381