This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 Image 𝑅 𝑦 ↔ 𝐴 Image 𝑅 𝑦 ) )
2 imaeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝐴 ) )
3 2 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑦 = ( 𝑅 “ 𝑥 ) ↔ 𝑦 = ( 𝑅 “ 𝐴 ) ) )
4 1 3 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 Image 𝑅 𝑦 ↔ 𝑦 = ( 𝑅 “ 𝑥 ) ) ↔ ( 𝐴 Image 𝑅 𝑦 ↔ 𝑦 = ( 𝑅 “ 𝐴 ) ) ) )
5 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 Image 𝑅 𝑦 ↔ 𝐴 Image 𝑅 𝐵 ) )
6 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝑅 “ 𝐴 ) ↔ 𝐵 = ( 𝑅 “ 𝐴 ) ) )
7 5 6 bibi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 Image 𝑅 𝑦 ↔ 𝑦 = ( 𝑅 “ 𝐴 ) ) ↔ ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) ) ) )
8 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 brimage ⊢ ( 𝑥 Image 𝑅 𝑦 ↔ 𝑦 = ( 𝑅 “ 𝑥 ) )
11 4 7 10 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) ) )