Theorem relinxp 5764

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

Syntax hints:   ∩ cin 3889   × cxp 5623  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-in 3897  df-ss 3907  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  inxp  5781  elinxp  5978  cnvcnv  6150  tpostpos  8193  brinxper  8670  erinxp  8735  brdom3  10448  brdom5  10449  brdom4  10450  fpwwe2lem7  10558  fpwwe2lem8  10559  fpwwe2lem11  10562  pwsle  17454  opsrtoslem2  22039  elrn3  35997  bj-idres  37527  br1cnvinxp  38633  inxprnres  38672  inxpss  38691  inxpss2  38695  iss2  38718  inxp2  38749  inxpxrn  38792