Theorem relinxp 5838

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

Syntax hints:   ∩ cin 3975   × cxp 5698  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  inxp  5856  elinxp  6048  cnvcnv  6223  tpostpos  8287  brinxper  8792  erinxp  8849  brdom3  10597  brdom5  10598  brdom4  10599  fpwwe2lem7  10706  fpwwe2lem8  10707  fpwwe2lem11  10710  pwsle  17552  opsrtoslem2  22103  elrn3  35724  bj-idres  37126  br1cnvinxp  38212  inxprnres  38248  inxpss  38267  inxpss2  38271  iss2  38300  inxp2  38323  inxpxrn  38351