Theorem sb56 2150

Description: Two equivalent ways of expressing the proper substitution of y for x in ph, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1881. The implication "to the left" is equs4 2290 and does not require any dv condition (but the version with a dv condition, equs4v 1930, requires fewer axioms). Theorem equs45f 2350 replaces the dv condition with a non-freeness hypothesis and equs5 2351 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2109 in place of equsex 2292 in order to remove dependency on ax-13 2246. (Revised by BJ, 20-Dec-2020.)

Assertion

Ref	Expression
sb56	|- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem sb56

Step	Hyp	Ref	Expression
1		nfa1 2028	. 2 |- F/ x A. x ( x = y -> ph )
2		ax12v2 2049	. . 3 |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
3		sp 2053	. . . 4 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
4	3	com12 32	. . 3 |- ( x = y -> ( A. x ( x = y -> ph ) -> ph ) )
5	2, 4	impbid 202	. 2 |- ( x = y -> ( ph <-> A. x ( x = y -> ph ) ) )
6	1, 5	equsexv 2109	1 |- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704

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-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  sb6  2429  sb5  2430  mopick  2535  alexeqg  3332  bj-sb3v  32756  bj-sb4v  32757  bj-sb6  32767  bj-sb5  32768  pm13.196a  38615