Theorem relinxp 5806

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

This proof depends on syntax axioms:   ∩ cin 3907   × cxp 5664  Rel wrel 5671

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-in 3915  df-ss 3925  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  inxp  5823  elinxp  6023  cnvcnv  6195  tpostpos  8251  brinxper  8733  erinxp  8798  brdom3  10530  brdom5  10531  brdom4  10532  fpwwe2lem7  10640  fpwwe2lem8  10641  fpwwe2lem11  10644  pwsle  17571  opsrtoslem2  22244  elrn3  36275  bj-idres  37845  br1cnvinxp  38949  inxprnres  38988  inxpss  39007  inxpss2  39011  iss2  39034  inxp2  39065  inxpxrn  39108