Metamath Proof Explorer


Theorem sbhypfOLD

Description: Obsolete version of sbhypf as of 25-Jan-2025. (Contributed by Raph Levien, 10-Apr-2004) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses sbhypf.1
|- F/ x ps
sbhypf.2
|- ( x = A -> ( ph <-> ps ) )
Assertion sbhypfOLD
|- ( y = A -> ( [ y / x ] ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 sbhypf.1
 |-  F/ x ps
2 sbhypf.2
 |-  ( x = A -> ( ph <-> ps ) )
3 eqeq1
 |-  ( x = y -> ( x = A <-> y = A ) )
4 3 equsexvw
 |-  ( E. x ( x = y /\ x = A ) <-> y = A )
5 nfs1v
 |-  F/ x [ y / x ] ph
6 5 1 nfbi
 |-  F/ x ( [ y / x ] ph <-> ps )
7 sbequ12
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
8 7 bicomd
 |-  ( x = y -> ( [ y / x ] ph <-> ph ) )
9 8 2 sylan9bb
 |-  ( ( x = y /\ x = A ) -> ( [ y / x ] ph <-> ps ) )
10 6 9 exlimi
 |-  ( E. x ( x = y /\ x = A ) -> ( [ y / x ] ph <-> ps ) )
11 4 10 sylbir
 |-  ( y = A -> ( [ y / x ] ph <-> ps ) )