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

Metamath Proof Explorer

Theorem reusv2

Description: Two ways to express single-valuedness of a class expression C ( y ) that is constant for those y e. B such that ph . The first antecedent ensures that the constant value belongs to the existential uniqueness domain A , and the second ensures that C ( y ) is evaluated for at least one y . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 nfrab1 
 |-  F/_ y { y e. B | ph }
2 nfcv 
 |-  F/_ z { y e. B | ph }
3 nfv 
 |-  F/ z C e. A
4 nfcsb1v 
 |-  F/_ y [_ z / y ]_ C
5 4 nfel1 
 |-  F/ y [_ z / y ]_ C e. A
6 csbeq1a 
 |-  ( y = z -> C = [_ z / y ]_ C )
7 6 eleq1d 
 |-  ( y = z -> ( C e. A <-> [_ z / y ]_ C e. A ) )
8 1 2 3 5 7 cbvralfw 
 |-  ( A. y e. { y e. B | ph } C e. A <-> A. z e. { y e. B | ph } [_ z / y ]_ C e. A )
9 rabid 
 |-  ( y e. { y e. B | ph } <-> ( y e. B /\ ph ) )
10 9 imbi1i 
 |-  ( ( y e. { y e. B | ph } -> C e. A ) <-> ( ( y e. B /\ ph ) -> C e. A ) )
11 impexp 
 |-  ( ( ( y e. B /\ ph ) -> C e. A ) <-> ( y e. B -> ( ph -> C e. A ) ) )
12 10 11 bitri 
 |-  ( ( y e. { y e. B | ph } -> C e. A ) <-> ( y e. B -> ( ph -> C e. A ) ) )
13 12 ralbii2 
 |-  ( A. y e. { y e. B | ph } C e. A <-> A. y e. B ( ph -> C e. A ) )
14 8 13 bitr3i 
 |-  ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A <-> A. y e. B ( ph -> C e. A ) )
15 rabn0 
 |-  ( { y e. B | ph } =/= (/) <-> E. y e. B ph )
16 reusv2lem5 
 |-  ( ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A /\ { y e. B | ph } =/= (/) ) -> ( E! x e. A E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A A. z e. { y e. B | ph } x = [_ z / y ]_ C ) )
17 nfv 
 |-  F/ z x = C
18 4 nfeq2 
 |-  F/ y x = [_ z / y ]_ C
19 6 eqeq2d 
 |-  ( y = z -> ( x = C <-> x = [_ z / y ]_ C ) )
20 1 2 17 18 19 cbvrexfw 
 |-  ( E. y e. { y e. B | ph } x = C <-> E. z e. { y e. B | ph } x = [_ z / y ]_ C )
21 9 anbi1i 
 |-  ( ( y e. { y e. B | ph } /\ x = C ) <-> ( ( y e. B /\ ph ) /\ x = C ) )
22 anass 
 |-  ( ( ( y e. B /\ ph ) /\ x = C ) <-> ( y e. B /\ ( ph /\ x = C ) ) )
23 21 22 bitri 
 |-  ( ( y e. { y e. B | ph } /\ x = C ) <-> ( y e. B /\ ( ph /\ x = C ) ) )
24 23 rexbii2 
 |-  ( E. y e. { y e. B | ph } x = C <-> E. y e. B ( ph /\ x = C ) )
25 20 24 bitr3i 
 |-  ( E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E. y e. B ( ph /\ x = C ) )
26 25 reubii 
 |-  ( E! x e. A E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A E. y e. B ( ph /\ x = C ) )
27 1 2 17 18 19 cbvralfw 
 |-  ( A. y e. { y e. B | ph } x = C <-> A. z e. { y e. B | ph } x = [_ z / y ]_ C )
28 9 imbi1i 
 |-  ( ( y e. { y e. B | ph } -> x = C ) <-> ( ( y e. B /\ ph ) -> x = C ) )
29 impexp 
 |-  ( ( ( y e. B /\ ph ) -> x = C ) <-> ( y e. B -> ( ph -> x = C ) ) )
30 28 29 bitri 
 |-  ( ( y e. { y e. B | ph } -> x = C ) <-> ( y e. B -> ( ph -> x = C ) ) )
31 30 ralbii2 
 |-  ( A. y e. { y e. B | ph } x = C <-> A. y e. B ( ph -> x = C ) )
32 27 31 bitr3i 
 |-  ( A. z e. { y e. B | ph } x = [_ z / y ]_ C <-> A. y e. B ( ph -> x = C ) )
33 32 reubii 
 |-  ( E! x e. A A. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A A. y e. B ( ph -> x = C ) )
34 16 26 33 3bitr3g 
 |-  ( ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A /\ { y e. B | ph } =/= (/) ) -> ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x e. A A. y e. B ( ph -> x = C ) ) )
35 14 15 34 syl2anbr 
 |-  ( ( A. y e. B ( ph -> C e. A ) /\ E. y e. B ph ) -> ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x e. A A. y e. B ( ph -> x = C ) ) )