Theorem equsexALT 2293

Description: Alternate proof of equsex 2292. This proves the result directly, instead of as a corollary of equsal 2291 via equs4 2290. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2246 is ax6e 2250. This proof mimics that of equsal 2291 (in particular, note that pm5.32i 669, exbii 1774, 19.41 2103, mpbiran 953 correspond respectively to pm5.74i 260, albii 1747, 19.23 2080, a1bi 352). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

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

Proof of Theorem equsexALT

Step	Hyp	Ref	Expression
1		equsal.2	. . . 4 |- ( x = y -> ( ph <-> ps ) )
2	1	pm5.32i 669	. . 3 |- ( ( x = y /\ ph ) <-> ( x = y /\ ps ) )
3	2	exbii 1774	. 2 |- ( E. x ( x = y /\ ph ) <-> E. x ( x = y /\ ps ) )
4		ax6e 2250	. . 3 |- E. x x = y
5		equsal.1	. . . 4 |- F/ x ps
6	5	19.41 2103	. . 3 |- ( E. x ( x = y /\ ps ) <-> ( E. x x = y /\ ps ) )
7	4, 6	mpbiran 953	. 2 |- ( E. x ( x = y /\ ps ) <-> ps )
8	3, 7	bitri 264	1 |- ( E. x ( x = y /\ ph ) <-> ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   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-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)