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