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 -> ( { (/) } X. tag A ) = ( { (/) } X. tag B ) )
2		df-bj-1upl	|- (| A |) = ( { (/) } X. tag A )
3		df-bj-1upl	|- (| B |) = ( { (/) } X. tag B )
4	1 2 3	3eqtr4g	|- ( A = B -> (| A |) = (| B |) )