Theorem sb6 1866

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 1865	. . 3 |- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
2	1	anbi2i 453	. 2 |- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( ( x = y -> ph ) /\ A. x ( x = y -> ph ) ) )
3		df-sb 1743	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4		ax-4 1490	. . 3 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
5	4	pm4.71ri 390	. 2 |- ( A. x ( x = y -> ph ) <-> ( ( x = y -> ph ) /\ A. x ( x = y -> ph ) ) )
6	2, 3, 5	3bitr4i 211	1 |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1333   E.wex 1472   [wsb 1742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-sb 1743

This theorem is referenced by:  sb5  1867  sbnv  1868  sbanv  1869  sbi1v  1871  sbi2v  1872  hbs1  1918  2sb6  1964  sbcom2v  1965  sb6a  1968  sb7af  1973  sbalyz  1979  sbal1yz  1981  exsb  1988  sbal2  2000  cbvabw  2280  nfabdw  2318  csbcow  3042