Theorem sbhypf 3253

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3552. (Contributed by Raph Levien, 10-Apr-2004.)

Hypotheses

Ref	Expression
sbhypf.1	|- F/ x ps
sbhypf.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
sbhypf	|- ( y = A -> ( [ y / x ] ph <-> ps ) )

Distinct variable groups:   x, A   x, y

Allowed substitution hints:   ph( x, y)   ps( x, y)   A( y)

Proof of Theorem sbhypf

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   F/wnf 1708   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615

This theorem is referenced by:  mob2  3386  reu2eqd  3403  cbvmptf  4748  ralxpf  5268  tfisi  7058  ac6sf  9311  nn0ind-raph  11477  ac6sf2  29429  nn0min  29567  ac6gf  33527  fdc1  33542