Metamath Proof Explorer


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