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=\left(x\in A⟼B\right)$$
	rnmptcOLD.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	rnmptcOLD.a	$$⊢\phi \to A\ne \varnothing$$
Assertion	rnmptcOLD	$$⊢\phi \to \mathrm{ran}F=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnmptcOLD.f	$$⊢F=\left(x\in A⟼B\right)$$
2		rnmptcOLD.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
3		rnmptcOLD.a	$$⊢\phi \to A\ne \varnothing$$
4		fconstmpt	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
5	1 4	eqtr4i	$$⊢F=A\times \left\{B\right\}$$
6	2 1	fmptd	$$⊢\phi \to F:A⟶C$$
7	6	ffnd	$$⊢\phi \to FFnA$$
8		fconst5	$$⊢\left(FFnA\wedge A\ne \varnothing \right)\to \left(F=A\times \left\{B\right\}\leftrightarrow \mathrm{ran}F=\left\{B\right\}\right)$$
9	7 3 8	syl2anc	$$⊢\phi \to \left(F=A\times \left\{B\right\}\leftrightarrow \mathrm{ran}F=\left\{B\right\}\right)$$
10	5 9	mpbii	$$⊢\phi \to \mathrm{ran}F=\left\{B\right\}$$