Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Logic and set theory
brabg2
Next ⟩
opelopab3
Metamath Proof Explorer
Ascii
Unicode
Theorem
brabg2
Description:
Relation by a binary relation abstraction.
(Contributed by
Jeff Madsen
, 2-Sep-2009)
Ref
Expression
Hypotheses
brabg2.1
⊢
x
=
A
→
φ
↔
ψ
brabg2.2
⊢
y
=
B
→
ψ
↔
χ
brabg2.3
⊢
R
=
x
y
|
φ
brabg2.4
⊢
χ
→
A
∈
C
Assertion
brabg2
⊢
B
∈
D
→
A
R
B
↔
χ
Proof
Step
Hyp
Ref
Expression
1
brabg2.1
⊢
x
=
A
→
φ
↔
ψ
2
brabg2.2
⊢
y
=
B
→
ψ
↔
χ
3
brabg2.3
⊢
R
=
x
y
|
φ
4
brabg2.4
⊢
χ
→
A
∈
C
5
3
relopabi
⊢
Rel
⁡
R
6
5
brrelex1i
⊢
A
R
B
→
A
∈
V
7
1
2
3
brabg
⊢
A
∈
V
∧
B
∈
D
→
A
R
B
↔
χ
8
7
biimpd
⊢
A
∈
V
∧
B
∈
D
→
A
R
B
→
χ
9
8
ex
⊢
A
∈
V
→
B
∈
D
→
A
R
B
→
χ
10
9
com3l
⊢
B
∈
D
→
A
R
B
→
A
∈
V
→
χ
11
6
10
mpdi
⊢
B
∈
D
→
A
R
B
→
χ
12
1
2
3
brabg
⊢
A
∈
C
∧
B
∈
D
→
A
R
B
↔
χ
13
12
exbiri
⊢
A
∈
C
→
B
∈
D
→
χ
→
A
R
B
14
13
com3l
⊢
B
∈
D
→
χ
→
A
∈
C
→
A
R
B
15
4
14
mpdi
⊢
B
∈
D
→
χ
→
A
R
B
16
11
15
impbid
⊢
B
∈
D
→
A
R
B
↔
χ