Theorem brimageg

Description: Closed form of brimage . (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	brimageg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\leftrightarrow B=R\left[A\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=A\to \left(x\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow A\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\right)$$
2		imaeq2	$$⊢x=A\to R\left[x\right]=R\left[A\right]$$
3	2	eqeq2d	$$⊢x=A\to \left(y=R\left[x\right]\leftrightarrow y=R\left[A\right]\right)$$
4	1 3	bibi12d	$$⊢x=A\to \left(\left(x\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow y=R\left[x\right]\right)\leftrightarrow \left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow y=R\left[A\right]\right)\right)$$
5		breq2	$$⊢y=B\to \left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\right)$$
6		eqeq1	$$⊢y=B\to \left(y=R\left[A\right]\leftrightarrow B=R\left[A\right]\right)$$
7	5 6	bibi12d	$$⊢y=B\to \left(\left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow y=R\left[A\right]\right)\leftrightarrow \left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\leftrightarrow B=R\left[A\right]\right)\right)$$
8		vex	$$⊢x\in \mathrm{V}$$
9		vex	$$⊢y\in \mathrm{V}$$
10	8 9	brimage	$$⊢x\mathrm{𝖨𝗆𝖺𝗀𝖾}Ry\leftrightarrow y=R\left[x\right]$$
11	4 7 10	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\leftrightarrow B=R\left[A\right]\right)$$