Theorem reuhypd

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd . (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	reuhypd.1	|- ( ( ph /\ x e. C ) -> B e. C )
	reuhypd.2	|- ( ( ph /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) )
Assertion	reuhypd	|- ( ( ph /\ x e. C ) -> E! y e. C x = A )

Proof

Step	Hyp	Ref	Expression
1		reuhypd.1	|- ( ( ph /\ x e. C ) -> B e. C )
2		reuhypd.2	|- ( ( ph /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) )
3	1	elexd	|- ( ( ph /\ x e. C ) -> B e. _V )
4		eueq	|- ( B e. _V <-> E! y y = B )
5	3 4	sylib	|- ( ( ph /\ x e. C ) -> E! y y = B )
6		eleq1	|- ( y = B -> ( y e. C <-> B e. C ) )
7	1 6	syl5ibrcom	|- ( ( ph /\ x e. C ) -> ( y = B -> y e. C ) )
8	7	pm4.71rd	|- ( ( ph /\ x e. C ) -> ( y = B <-> ( y e. C /\ y = B ) ) )
9	2	3expa	|- ( ( ( ph /\ x e. C ) /\ y e. C ) -> ( x = A <-> y = B ) )
10	9	pm5.32da	|- ( ( ph /\ x e. C ) -> ( ( y e. C /\ x = A ) <-> ( y e. C /\ y = B ) ) )
11	8 10	bitr4d	|- ( ( ph /\ x e. C ) -> ( y = B <-> ( y e. C /\ x = A ) ) )
12	11	eubidv	|- ( ( ph /\ x e. C ) -> ( E! y y = B <-> E! y ( y e. C /\ x = A ) ) )
13	5 12	mpbid	|- ( ( ph /\ x e. C ) -> E! y ( y e. C /\ x = A ) )
14		df-reu	|- ( E! y e. C x = A <-> E! y ( y e. C /\ x = A ) )
15	13 14	sylibr	|- ( ( ph /\ x e. C ) -> E! y e. C x = A )