Theorem ralrnmpo

Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	rngop.1	|- F = ( x e. A , y e. B |-> C )
	ralrnmpo.2	|- ( z = C -> ( ph <-> ps ) )
Assertion	ralrnmpo	|- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		rngop.1	|- F = ( x e. A , y e. B |-> C )
2		ralrnmpo.2	|- ( z = C -> ( ph <-> ps ) )
3	1	rnmpo	|- ran F = { w | E. x e. A E. y e. B w = C }
4	3	raleqi	|- ( A. z e. ran F ph <-> A. z e. { w | E. x e. A E. y e. B w = C } ph )
5		eqeq1	|- ( w = z -> ( w = C <-> z = C ) )
6	5	2rexbidv	|- ( w = z -> ( E. x e. A E. y e. B w = C <-> E. x e. A E. y e. B z = C ) )
7	6	ralab	|- ( A. z e. { w | E. x e. A E. y e. B w = C } ph <-> A. z ( E. x e. A E. y e. B z = C -> ph ) )
8		ralcom4	|- ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. z A. x e. A ( E. y e. B z = C -> ph ) )
9		r19.23v	|- ( A. x e. A ( E. y e. B z = C -> ph ) <-> ( E. x e. A E. y e. B z = C -> ph ) )
10	9	albii	|- ( A. z A. x e. A ( E. y e. B z = C -> ph ) <-> A. z ( E. x e. A E. y e. B z = C -> ph ) )
11	8 10	bitr2i	|- ( A. z ( E. x e. A E. y e. B z = C -> ph ) <-> A. x e. A A. z ( E. y e. B z = C -> ph ) )
12	4 7 11	3bitri	|- ( A. z e. ran F ph <-> A. x e. A A. z ( E. y e. B z = C -> ph ) )
13		ralcom4	|- ( A. y e. B A. z ( z = C -> ph ) <-> A. z A. y e. B ( z = C -> ph ) )
14		r19.23v	|- ( A. y e. B ( z = C -> ph ) <-> ( E. y e. B z = C -> ph ) )
15	14	albii	|- ( A. z A. y e. B ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) )
16	13 15	bitri	|- ( A. y e. B A. z ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) )
17		nfv	|- F/ z ps
18	17 2	ceqsalg	|- ( C e. V -> ( A. z ( z = C -> ph ) <-> ps ) )
19	18	ralimi	|- ( A. y e. B C e. V -> A. y e. B ( A. z ( z = C -> ph ) <-> ps ) )
20		ralbi	|- ( A. y e. B ( A. z ( z = C -> ph ) <-> ps ) -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) )
21	19 20	syl	|- ( A. y e. B C e. V -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) )
22	16 21	bitr3id	|- ( A. y e. B C e. V -> ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) )
23	22	ralimi	|- ( A. x e. A A. y e. B C e. V -> A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) )
24		ralbi	|- ( A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) )
25	23 24	syl	|- ( A. x e. A A. y e. B C e. V -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) )
26	12 25	syl5bb	|- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) )