Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
inxp2
Next ⟩
opabf
Metamath Proof Explorer
Ascii
Unicode
Theorem
inxp2
Description:
Intersection with a Cartesian product.
(Contributed by
Peter Mazsa
, 18-Jul-2019)
Ref
Expression
Assertion
inxp2
⊢
R
∩
A
×
B
=
x
y
|
x
∈
A
∧
y
∈
B
∧
x
R
y
Proof
Step
Hyp
Ref
Expression
1
relinxp
⊢
Rel
⁡
R
∩
A
×
B
2
dfrel4v
⊢
Rel
⁡
R
∩
A
×
B
↔
R
∩
A
×
B
=
x
y
|
x
R
∩
A
×
B
y
3
1
2
mpbi
⊢
R
∩
A
×
B
=
x
y
|
x
R
∩
A
×
B
y
4
brinxp2
⊢
x
R
∩
A
×
B
y
↔
x
∈
A
∧
y
∈
B
∧
x
R
y
5
4
opabbii
⊢
x
y
|
x
R
∩
A
×
B
y
=
x
y
|
x
∈
A
∧
y
∈
B
∧
x
R
y
6
3
5
eqtri
⊢
R
∩
A
×
B
=
x
y
|
x
∈
A
∧
y
∈
B
∧
x
R
y