Theorem relmpoopab

Description: Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		relmpoopab.1	$$⊢F=\left(x\in A,y\in B⟼\left\{⟨z,w⟩|\phi \right\}\right)$$
2		relopabv	$$⊢\mathrm{Rel}\left\{⟨z,w⟩|\phi \right\}$$
3		df-rel	$$⊢\mathrm{Rel}\left\{⟨z,w⟩|\phi \right\}\leftrightarrow \left\{⟨z,w⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	mpbi	$$⊢\left\{⟨z,w⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
5	4	rgen2w	$$⊢\forall x\in A\forall y\in B\left\{⟨z,w⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
6	1	ovmptss	$$⊢\forall x\in A\forall y\in B\left\{⟨z,w⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}\to CFD\subseteq \mathrm{V}\times \mathrm{V}$$
7	5 6	ax-mp	$$⊢CFD\subseteq \mathrm{V}\times \mathrm{V}$$
8		df-rel	$$⊢\mathrm{Rel}\left(CFD\right)\leftrightarrow CFD\subseteq \mathrm{V}\times \mathrm{V}$$
9	7 8	mpbir	$$⊢\mathrm{Rel}\left(CFD\right)$$