Theorem elrnmpo

Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	rngop.1	|- F = ( x e. A , y e. B |-> C )
	elrnmpo.1	|- C e. _V
Assertion	elrnmpo	|- ( D e. ran F <-> E. x e. A E. y e. B D = C )

Proof

Step	Hyp	Ref	Expression
1		rngop.1	|- F = ( x e. A , y e. B |-> C )
2		elrnmpo.1	|- C e. _V
3	1	rnmpo	|- ran F = { z | E. x e. A E. y e. B z = C }
4	3	eleq2i	|- ( D e. ran F <-> D e. { z | E. x e. A E. y e. B z = C } )
5		eleq1	|- ( D = C -> ( D e. _V <-> C e. _V ) )
6	2 5	mpbiri	|- ( D = C -> D e. _V )
7	6	rexlimivw	|- ( E. y e. B D = C -> D e. _V )
8	7	rexlimivw	|- ( E. x e. A E. y e. B D = C -> D e. _V )
9		eqeq1	|- ( z = D -> ( z = C <-> D = C ) )
10	9	2rexbidv	|- ( z = D -> ( E. x e. A E. y e. B z = C <-> E. x e. A E. y e. B D = C ) )
11	8 10	elab3	|- ( D e. { z | E. x e. A E. y e. B z = C } <-> E. x e. A E. y e. B D = C )
12	4 11	bitri	|- ( D e. ran F <-> E. x e. A E. y e. B D = C )