Theorem rnmptpr

Description: Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnmptpr.a	|- ( ph -> A e. V )
	rnmptpr.b	|- ( ph -> B e. W )
	rnmptpr.f	|- F = ( x e. { A , B } |-> C )
	rnmptpr.d	|- ( x = A -> C = D )
	rnmptpr.e	|- ( x = B -> C = E )
Assertion	rnmptpr	|- ( ph -> ran F = { D , E } )

Proof

Step	Hyp	Ref	Expression
1		rnmptpr.a	|- ( ph -> A e. V )
2		rnmptpr.b	|- ( ph -> B e. W )
3		rnmptpr.f	|- F = ( x e. { A , B } |-> C )
4		rnmptpr.d	|- ( x = A -> C = D )
5		rnmptpr.e	|- ( x = B -> C = E )
6	4	eqeq2d	|- ( x = A -> ( y = C <-> y = D ) )
7	5	eqeq2d	|- ( x = B -> ( y = C <-> y = E ) )
8	6 7	rexprg	|- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } y = C <-> ( y = D \/ y = E ) ) )
9	1 2 8	syl2anc	|- ( ph -> ( E. x e. { A , B } y = C <-> ( y = D \/ y = E ) ) )
10	3	elrnmpt	|- ( y e. _V -> ( y e. ran F <-> E. x e. { A , B } y = C ) )
11	10	elv	|- ( y e. ran F <-> E. x e. { A , B } y = C )
12		vex	|- y e. _V
13	12	elpr	|- ( y e. { D , E } <-> ( y = D \/ y = E ) )
14	9 11 13	3bitr4g	|- ( ph -> ( y e. ran F <-> y e. { D , E } ) )
15	14	eqrdv	|- ( ph -> ran F = { D , E } )