Theorem sb6 1901

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 1900	. . 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 1777	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4		ax-4 1524	. . 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 1362   E.wex 1506   [wsb 1776

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  sb5  1902  sbnv  1903  sbanv  1904  sbi1v  1906  sbi2v  1907  hbs1  1957  2sb6  2003  sbcom2v  2004  sb6a  2007  sb7af  2012  sbalyz  2018  sbal1yz  2020  exsb  2027  sbal2  2039  cbvabw  2319  nfabdw  2358  csbcow  3095