Theorem relinxp 5780

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

Syntax hints:   ∩ cin 3916   × cxp 5639  Rel wrel 5646

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  inxp  5798  elinxp  5993  cnvcnv  6168  tpostpos  8228  brinxper  8703  erinxp  8767  brdom3  10488  brdom5  10489  brdom4  10490  fpwwe2lem7  10597  fpwwe2lem8  10598  fpwwe2lem11  10601  pwsle  17462  opsrtoslem2  21970  elrn3  35756  bj-idres  37155  br1cnvinxp  38252  inxprnres  38287  inxpss  38306  inxpss2  38310  iss2  38333  inxp2  38356  inxpxrn  38388