Metamath Proof Explorer


Theorem wl-equsb4

Description: Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable constraint. (Contributed by Wolf Lammen, 26-Jun-2019)

Ref Expression
Assertion wl-equsb4
|- ( -. A. x x = z -> ( [ y / x ] y = z <-> y = z ) )

Proof

Step Hyp Ref Expression
1 nfeqf
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y = z )
2 1 ex
 |-  ( -. A. x x = y -> ( -. A. x x = z -> F/ x y = z ) )
3 sbft
 |-  ( F/ x y = z -> ( [ y / x ] y = z <-> y = z ) )
4 2 3 syl6com
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( [ y / x ] y = z <-> y = z ) ) )
5 sbequ12r
 |-  ( y = x -> ( [ y / x ] y = z <-> y = z ) )
6 5 equcoms
 |-  ( x = y -> ( [ y / x ] y = z <-> y = z ) )
7 6 sps
 |-  ( A. x x = y -> ( [ y / x ] y = z <-> y = z ) )
8 4 7 pm2.61d2
 |-  ( -. A. x x = z -> ( [ y / x ] y = z <-> y = z ) )