Theorem equsex 2292

Description: An equivalence related to implicit substitution. See equsexvw 1932 and equsexv 2109 for versions with dv conditions proved from fewer axioms. See also the dual form equsal 2291. See equsexALT 2293 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.)

Hypotheses

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

Assertion

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

Proof of Theorem equsex

Step	Hyp	Ref	Expression
1		equsal.1	. . 3 |- F/ x ps
2		equsal.2	. . . 4 |- ( x = y -> ( ph <-> ps ) )
3	2	biimpa 501	. . 3 |- ( ( x = y /\ ph ) -> ps )
4	1, 3	exlimi 2086	. 2 |- ( E. x ( x = y /\ ph ) -> ps )
5	1, 2	equsal 2291	. . 3 |- ( A. x ( x = y -> ph ) <-> ps )
6		equs4 2290	. . 3 |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
7	5, 6	sylbir 225	. 2 |- ( ps -> E. x ( x = y /\ ph ) )
8	4, 7	impbii 199	1 |- ( E. x ( x = y /\ ph ) <-> ps )

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

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-12 2047  ax-13 2246

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:  equsexh  2295  sb5rf  2422