Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
residpr
Next ⟩
dfmpt
Metamath Proof Explorer
Ascii
Unicode
Theorem
residpr
Description:
Restriction of the identity to a pair.
(Contributed by
AV
, 11-Dec-2018)
Ref
Expression
Assertion
residpr
⊢
A
∈
V
∧
B
∈
W
→
I
↾
A
B
=
A
A
B
B
Proof
Step
Hyp
Ref
Expression
1
df-pr
⊢
A
B
=
A
∪
B
2
1
reseq2i
⊢
I
↾
A
B
=
I
↾
A
∪
B
3
resundi
⊢
I
↾
A
∪
B
=
I
↾
A
∪
I
↾
B
4
2
3
eqtri
⊢
I
↾
A
B
=
I
↾
A
∪
I
↾
B
5
xpsng
⊢
A
∈
V
∧
A
∈
V
→
A
×
A
=
A
A
6
5
anidms
⊢
A
∈
V
→
A
×
A
=
A
A
7
6
adantr
⊢
A
∈
V
∧
B
∈
W
→
A
×
A
=
A
A
8
xpsng
⊢
B
∈
W
∧
B
∈
W
→
B
×
B
=
B
B
9
8
anidms
⊢
B
∈
W
→
B
×
B
=
B
B
10
9
adantl
⊢
A
∈
V
∧
B
∈
W
→
B
×
B
=
B
B
11
7
10
uneq12d
⊢
A
∈
V
∧
B
∈
W
→
A
×
A
∪
B
×
B
=
A
A
∪
B
B
12
restidsing
⊢
I
↾
A
=
A
×
A
13
restidsing
⊢
I
↾
B
=
B
×
B
14
12
13
uneq12i
⊢
I
↾
A
∪
I
↾
B
=
A
×
A
∪
B
×
B
15
df-pr
⊢
A
A
B
B
=
A
A
∪
B
B
16
11
14
15
3eqtr4g
⊢
A
∈
V
∧
B
∈
W
→
I
↾
A
∪
I
↾
B
=
A
A
B
B
17
4
16
syl5eq
⊢
A
∈
V
∧
B
∈
W
→
I
↾
A
B
=
A
A
B
B