Metamath Proof Explorer


Theorem eqsbc1

Description: Substitution for the left-hand side in an equality. Class version of eqsb1 . (Contributed by Andrew Salmon, 29-Jun-2011) Avoid ax-13 . (Revised by Wolf Lammen, 29-Apr-2023)

Ref Expression
Assertion eqsbc1 AV[˙A/x]˙x=BA=B

Proof

Step Hyp Ref Expression
1 dfsbcq y=A[˙y/x]˙x=B[˙A/x]˙x=B
2 eqeq1 y=Ay=BA=B
3 sbsbc yxx=B[˙y/x]˙x=B
4 eqsb1 yxx=By=B
5 3 4 bitr3i [˙y/x]˙x=By=B
6 1 2 5 vtoclbg AV[˙A/x]˙x=BA=B