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 ) ) )