Theorem relinxp 5791

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

This proof depends on syntax axioms:   ∩ cin 4089   × cxp 5648  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  inxp  5808  elinxp  6007  cnvcnv  6183  tpostpos  8266  brinxper  8750  erinxp  8815  brdom3  10610  brdom5  10611  brdom4  10612  fpwwe2lem7  10725  fpwwe2lem8  10726  fpwwe2lem11  10729  pwsle  17669  opsrtoslem2  22370  cgraer  29382  elrn3  36619  bj-idres  38174  br1cnvinxp  39284  inxprnres  39323  inxpss  39342  inxpss2  39346  iss2  39369  inxp2  39400  inxpxrn  39443