Theorem relmptopab

Description: Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	relmptopab.1	$$⊢F=\left(x\in A⟼\left\{⟨y,z⟩|\phi \right\}\right)$$
Assertion	relmptopab	$$⊢\mathrm{Rel}F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		relmptopab.1	$$⊢F=\left(x\in A⟼\left\{⟨y,z⟩|\phi \right\}\right)$$
2	1	fvmptss	$$⊢\forall x\in A\left\{⟨y,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}\to F\left(B\right)\subseteq \mathrm{V}\times \mathrm{V}$$
3		relopab	$$⊢\mathrm{Rel}\left\{⟨y,z⟩|\phi \right\}$$
4		df-rel	$$⊢\mathrm{Rel}\left\{⟨y,z⟩|\phi \right\}\leftrightarrow \left\{⟨y,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
5	3 4	mpbi	$$⊢\left\{⟨y,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
6	5	a1i	$$⊢x\in A\to \left\{⟨y,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
7	2 6	mprg	$$⊢F\left(B\right)\subseteq \mathrm{V}\times \mathrm{V}$$
8		df-rel	$$⊢\mathrm{Rel}F\left(B\right)\leftrightarrow F\left(B\right)\subseteq \mathrm{V}\times \mathrm{V}$$
9	7 8	mpbir	$$⊢\mathrm{Rel}F\left(B\right)$$