Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Tuples of classes
bj-1upleq
Next ⟩
bj-cpr1
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-1upleq
Description:
Substitution property for
(| - |)
.
(Contributed by
BJ
, 6-Apr-2019)
Ref
Expression
Assertion
bj-1upleq
⊢
A
=
B
→
A
=
B
Proof
Step
Hyp
Ref
Expression
1
bj-xtageq
⊢
A
=
B
→
∅
×
tag
A
=
∅
×
tag
B
2
df-bj-1upl
⊢
A
=
∅
×
tag
A
3
df-bj-1upl
⊢
B
=
∅
×
tag
B
4
1
2
3
3eqtr4g
⊢
A
=
B
→
A
=
B