Metamath Proof Explorer


Theorem bj-2upleq

Description: Substitution property for (| - ,, - |) . (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-2upleq A=BC=DAC=BD

Proof

Step Hyp Ref Expression
1 bj-1upleq A=BA=B
2 bj-xtageq C=D1𝑜×tagC=1𝑜×tagD
3 uneq12 A=B1𝑜×tagC=1𝑜×tagDA1𝑜×tagC=B1𝑜×tagD
4 3 ex A=B1𝑜×tagC=1𝑜×tagDA1𝑜×tagC=B1𝑜×tagD
5 1 2 4 syl2im A=BC=DA1𝑜×tagC=B1𝑜×tagD
6 df-bj-2upl AC=A1𝑜×tagC
7 df-bj-2upl BD=B1𝑜×tagD
8 6 7 eqeq12i AC=BDA1𝑜×tagC=B1𝑜×tagD
9 5 8 syl6ibr A=BC=DAC=BD