Metamath Proof Explorer

Theorem reusv3

Description: Two ways to express single-valuedness of a class expression C ( y ) . See reusv1 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012)

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

Proof

Step Hyp Ref Expression
1 reusv3.1 
 |-  ( y = z -> ( ph <-> ps ) )
2 reusv3.2 
 |-  ( y = z -> C = D )
3 2 eleq1d 
 |-  ( y = z -> ( C e. A <-> D e. A ) )
4 1 3 anbi12d 
 |-  ( y = z -> ( ( ph /\ C e. A ) <-> ( ps /\ D e. A ) ) )
5 4 cbvrexvw 
 |-  ( E. y e. B ( ph /\ C e. A ) <-> E. z e. B ( ps /\ D e. A ) )
6 nfra2w 
 |-  F/ z A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D )
7 nfv 
 |-  F/ z E. x e. A A. y e. B ( ph -> x = C )
8 6 7 nfim 
 |-  F/ z ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) )
9 risset 
 |-  ( D e. A <-> E. x e. A x = D )
10 ralcom 
 |-  ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) <-> A. z e. B A. y e. B ( ( ph /\ ps ) -> C = D ) )
11 impexp 
 |-  ( ( ( ph /\ ps ) -> C = D ) <-> ( ph -> ( ps -> C = D ) ) )
12 bi2.04 
 |-  ( ( ph -> ( ps -> C = D ) ) <-> ( ps -> ( ph -> C = D ) ) )
13 11 12 bitri 
 |-  ( ( ( ph /\ ps ) -> C = D ) <-> ( ps -> ( ph -> C = D ) ) )
14 13 ralbii 
 |-  ( A. y e. B ( ( ph /\ ps ) -> C = D ) <-> A. y e. B ( ps -> ( ph -> C = D ) ) )
15 r19.21v 
 |-  ( A. y e. B ( ps -> ( ph -> C = D ) ) <-> ( ps -> A. y e. B ( ph -> C = D ) ) )
16 14 15 bitri 
 |-  ( A. y e. B ( ( ph /\ ps ) -> C = D ) <-> ( ps -> A. y e. B ( ph -> C = D ) ) )
17 16 ralbii 
 |-  ( A. z e. B A. y e. B ( ( ph /\ ps ) -> C = D ) <-> A. z e. B ( ps -> A. y e. B ( ph -> C = D ) ) )
18 10 17 bitri 
 |-  ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) <-> A. z e. B ( ps -> A. y e. B ( ph -> C = D ) ) )
19 rsp 
 |-  ( A. z e. B ( ps -> A. y e. B ( ph -> C = D ) ) -> ( z e. B -> ( ps -> A. y e. B ( ph -> C = D ) ) ) )
20 18 19 sylbi 
 |-  ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> ( z e. B -> ( ps -> A. y e. B ( ph -> C = D ) ) ) )
21 20 com3l 
 |-  ( z e. B -> ( ps -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> A. y e. B ( ph -> C = D ) ) ) )
22 21 imp31 
 |-  ( ( ( z e. B /\ ps ) /\ A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) ) -> A. y e. B ( ph -> C = D ) )
23 eqeq1 
 |-  ( x = D -> ( x = C <-> D = C ) )
24 eqcom 
 |-  ( D = C <-> C = D )
25 23 24 bitrdi 
 |-  ( x = D -> ( x = C <-> C = D ) )
26 25 imbi2d 
 |-  ( x = D -> ( ( ph -> x = C ) <-> ( ph -> C = D ) ) )
27 26 ralbidv 
 |-  ( x = D -> ( A. y e. B ( ph -> x = C ) <-> A. y e. B ( ph -> C = D ) ) )
28 22 27 syl5ibrcom 
 |-  ( ( ( z e. B /\ ps ) /\ A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) ) -> ( x = D -> A. y e. B ( ph -> x = C ) ) )
29 28 reximdv 
 |-  ( ( ( z e. B /\ ps ) /\ A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) ) -> ( E. x e. A x = D -> E. x e. A A. y e. B ( ph -> x = C ) ) )
30 29 ex 
 |-  ( ( z e. B /\ ps ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> ( E. x e. A x = D -> E. x e. A A. y e. B ( ph -> x = C ) ) ) )
31 30 com23 
 |-  ( ( z e. B /\ ps ) -> ( E. x e. A x = D -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) ) ) )
32 9 31 biimtrid 
 |-  ( ( z e. B /\ ps ) -> ( D e. A -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) ) ) )
33 32 expimpd 
 |-  ( z e. B -> ( ( ps /\ D e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) ) ) )
34 8 33 rexlimi 
 |-  ( E. z e. B ( ps /\ D e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) ) )
35 5 34 sylbi 
 |-  ( E. y e. B ( ph /\ C e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) -> E. x e. A A. y e. B ( ph -> x = C ) ) )
36 1 2 reusv3i 
 |-  ( E. x e. A A. y e. B ( ph -> x = C ) -> A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) )
37 35 36 impbid1 
 |-  ( E. y e. B ( ph /\ C e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )