Theorem relinxp 5751

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

Syntax hints:   ∩ cin 3898   × cxp 5611  Rel wrel 5618

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 3393  df-v 3435  df-in 3906  df-ss 3916  df-opab 5151  df-xp 5619  df-rel 5620

This theorem is referenced by:  inxp  5768  elinxp  5964  cnvcnv  6135  tpostpos  8170  brinxper  8645  erinxp  8709  brdom3  10410  brdom5  10411  brdom4  10412  fpwwe2lem7  10519  fpwwe2lem8  10520  fpwwe2lem11  10523  pwsle  17383  opsrtoslem2  21945  elrn3  35752  bj-idres  37151  br1cnvinxp  38248  inxprnres  38283  inxpss  38302  inxpss2  38306  iss2  38329  inxp2  38352  inxpxrn  38384