Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Quantifier-free definitions
brdomaing
Next ⟩
brrangeg
Metamath Proof Explorer
Ascii
Unicode
Theorem
brdomaing
Description:
Closed form of
brdomain
.
(Contributed by
Scott Fenton
, 2-May-2014)
Ref
Expression
Assertion
brdomaing
⊢
A
∈
V
∧
B
∈
W
→
A
𝖣𝗈𝗆𝖺𝗂𝗇
B
↔
B
=
dom
⁡
A
Proof
Step
Hyp
Ref
Expression
1
breq1
⊢
a
=
A
→
a
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
A
𝖣𝗈𝗆𝖺𝗂𝗇
b
2
dmeq
⊢
a
=
A
→
dom
⁡
a
=
dom
⁡
A
3
2
eqeq2d
⊢
a
=
A
→
b
=
dom
⁡
a
↔
b
=
dom
⁡
A
4
1
3
bibi12d
⊢
a
=
A
→
a
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
b
=
dom
⁡
a
↔
A
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
b
=
dom
⁡
A
5
breq2
⊢
b
=
B
→
A
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
A
𝖣𝗈𝗆𝖺𝗂𝗇
B
6
eqeq1
⊢
b
=
B
→
b
=
dom
⁡
A
↔
B
=
dom
⁡
A
7
5
6
bibi12d
⊢
b
=
B
→
A
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
b
=
dom
⁡
A
↔
A
𝖣𝗈𝗆𝖺𝗂𝗇
B
↔
B
=
dom
⁡
A
8
vex
⊢
a
∈
V
9
vex
⊢
b
∈
V
10
8
9
brdomain
⊢
a
𝖣𝗈𝗆𝖺𝗂𝗇
b
↔
b
=
dom
⁡
a
11
4
7
10
vtocl2g
⊢
A
∈
V
∧
B
∈
W
→
A
𝖣𝗈𝗆𝖺𝗂𝗇
B
↔
B
=
dom
⁡
A