Theorem relinxp 5792

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

This proof depends on syntax axioms:   ∩ cin 3898   × cxp 5649  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  inxp  5809  elinxp  6010  cnvcnv  6183  tpostpos  8247  brinxper  8731  erinxp  8796  brdom3  10588  brdom5  10589  brdom4  10590  fpwwe2lem7  10703  fpwwe2lem8  10704  fpwwe2lem11  10707  pwsle  17644  opsrtoslem2  22345  cgraer  29359  elrn3  36496  bj-idres  38049  br1cnvinxp  39159  inxprnres  39198  inxpss  39217  inxpss2  39221  iss2  39244  inxp2  39275  inxpxrn  39318