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 )