Metamath Proof Explorer


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