This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )