Theorem brimage

Description: Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brimage.1	⊢ 𝐴 ∈ V
	brimage.2	⊢ 𝐵 ∈ V
Assertion	brimage	⊢ ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		brimage.1	⊢ 𝐴 ∈ V
2		brimage.2	⊢ 𝐵 ∈ V
3		df-image	⊢ Image 𝑅 = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝑅 ) ⊗ V ) ) )
4		brxp	⊢ ( 𝐴 ( V × V ) 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5	1 2 4	mpbir2an	⊢ 𝐴 ( V × V ) 𝐵
6		vex	⊢ 𝑥 ∈ V
7		vex	⊢ 𝑦 ∈ V
8	6 7	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
9	8	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ◡ 𝑅 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 𝑅 𝑥 )
10	6 1	coep	⊢ ( 𝑥 ( E ∘ ◡ 𝑅 ) 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ◡ 𝑅 𝑦 )
11	6	elima	⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑦 𝑅 𝑥 )
12	9 10 11	3bitr4ri	⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐴 ) ↔ 𝑥 ( E ∘ ◡ 𝑅 ) 𝐴 )
13	1 2 3 5 12	brtxpsd3	⊢ ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) )