Theorem rnmptcOLD

Description: Obsolete version of rnmptc as of 17-Apr-2024. (Contributed by Glauco Siliprandi, 11-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rnmptcOLD.f	|- F = ( x e. A |-> B )
	rnmptcOLD.b	|- ( ( ph /\ x e. A ) -> B e. C )
	rnmptcOLD.a	|- ( ph -> A =/= (/) )
Assertion	rnmptcOLD	|- ( ph -> ran F = { B } )

Proof

Step	Hyp	Ref	Expression
1		rnmptcOLD.f	|- F = ( x e. A |-> B )
2		rnmptcOLD.b	|- ( ( ph /\ x e. A ) -> B e. C )
3		rnmptcOLD.a	|- ( ph -> A =/= (/) )
4		fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )
5	1 4	eqtr4i	|- F = ( A X. { B } )
6	2 1	fmptd	|- ( ph -> F : A --> C )
7	6	ffnd	|- ( ph -> F Fn A )
8		fconst5	|- ( ( F Fn A /\ A =/= (/) ) -> ( F = ( A X. { B } ) <-> ran F = { B } ) )
9	7 3 8	syl2anc	|- ( ph -> ( F = ( A X. { B } ) <-> ran F = { B } ) )
10	5 9	mpbii	|- ( ph -> ran F = { B } )