Theorem sb6 1886

Description: Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)

Assertion

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

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem sb6

Step	Hyp	Ref	Expression
1		sb56 1885	. . 3 |- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
2	1	anbi2i 457	. 2 |- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( ( x = y -> ph ) /\ A. x ( x = y -> ph ) ) )
3		df-sb 1763	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4		ax-4 1510	. . 3 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
5	4	pm4.71ri 392	. 2 |- ( A. x ( x = y -> ph ) <-> ( ( x = y -> ph ) /\ A. x ( x = y -> ph ) ) )
6	2, 3, 5	3bitr4i 212	1 |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1351   E.wex 1492   [wsb 1762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-sb 1763

This theorem is referenced by:  sb5  1887  sbnv  1888  sbanv  1889  sbi1v  1891  sbi2v  1892  hbs1  1938  2sb6  1984  sbcom2v  1985  sb6a  1988  sb7af  1993  sbalyz  1999  sbal1yz  2001  exsb  2008  sbal2  2020  cbvabw  2300  nfabdw  2338  csbcow  3068