Theorem relinxp 5803

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

Syntax hints:   ∩ cin 3905   × cxp 5661  Rel wrel 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  inxp  5820  elinxp  6020  cnvcnv  6192  tpostpos  8243  brinxper  8725  erinxp  8790  brdom3  10513  brdom5  10514  brdom4  10515  fpwwe2lem7  10623  fpwwe2lem8  10624  fpwwe2lem11  10627  pwsle  17547  opsrtoslem2  22188  elrn3  36232  bj-idres  37782  br1cnvinxp  38886  inxprnres  38925  inxpss  38944  inxpss2  38948  iss2  38971  inxp2  39002  inxpxrn  39045