Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Tuples of classes
bj-pr2eq
Next ⟩
bj-pr2un
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-pr2eq
Description:
Substitution property for
pr2
.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-pr2eq
⊢
A
=
B
→
pr2
A
=
pr2
B
Proof
Step
Hyp
Ref
Expression
1
bj-projeq2
⊢
A
=
B
→
1
𝑜
Proj
A
=
1
𝑜
Proj
B
2
df-bj-pr2
⊢
pr2
A
=
1
𝑜
Proj
A
3
df-bj-pr2
⊢
pr2
B
=
1
𝑜
Proj
B
4
1
2
3
3eqtr4g
⊢
A
=
B
→
pr2
A
=
pr2
B