Theorem brfullfun

Description: A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brfullfun.1	$$⊢A\in \mathrm{V}$$
	brfullfun.2	$$⊢B\in \mathrm{V}$$
Assertion	brfullfun	$$⊢A\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FB\leftrightarrow B=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		brfullfun.1	$$⊢A\in \mathrm{V}$$
2		brfullfun.2	$$⊢B\in \mathrm{V}$$
3		eqcom	$$⊢\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)=B\leftrightarrow B=\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)$$
4		fullfunfnv	$$⊢\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FFn\mathrm{V}$$
5		fnbrfvb	$$⊢\left(\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FFn\mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)=B\leftrightarrow A\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FB\right)$$
6	4 1 5	mp2an	$$⊢\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)=B\leftrightarrow A\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FB$$
7		fullfunfv	$$⊢\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)=F\left(A\right)$$
8	7	eqeq2i	$$⊢B=\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F\left(A\right)\leftrightarrow B=F\left(A\right)$$
9	3 6 8	3bitr3i	$$⊢A\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}FB\leftrightarrow B=F\left(A\right)$$