Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Tuples of classes
bj-2upleq
Next ⟩
bj-pr21val
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-2upleq
Description:
Substitution property for
(| - ,, - |)
.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-2upleq
⊢
A
=
B
→
C
=
D
→
A
C
=
B
D
Proof
Step
Hyp
Ref
Expression
1
bj-1upleq
⊢
A
=
B
→
A
=
B
2
bj-xtageq
⊢
C
=
D
→
1
𝑜
×
tag
C
=
1
𝑜
×
tag
D
3
uneq12
⊢
A
=
B
∧
1
𝑜
×
tag
C
=
1
𝑜
×
tag
D
→
A
∪
1
𝑜
×
tag
C
=
B
∪
1
𝑜
×
tag
D
4
3
ex
⊢
A
=
B
→
1
𝑜
×
tag
C
=
1
𝑜
×
tag
D
→
A
∪
1
𝑜
×
tag
C
=
B
∪
1
𝑜
×
tag
D
5
1
2
4
syl2im
⊢
A
=
B
→
C
=
D
→
A
∪
1
𝑜
×
tag
C
=
B
∪
1
𝑜
×
tag
D
6
df-bj-2upl
⊢
A
C
=
A
∪
1
𝑜
×
tag
C
7
df-bj-2upl
⊢
B
D
=
B
∪
1
𝑜
×
tag
D
8
6
7
eqeq12i
⊢
A
C
=
B
D
↔
A
∪
1
𝑜
×
tag
C
=
B
∪
1
𝑜
×
tag
D
9
5
8
syl6ibr
⊢
A
=
B
→
C
=
D
→
A
C
=
B
D