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 ⊢ A ∈ V ∧ B ∈ W → A 𝖨𝗆𝖺𝗀𝖾 R B ↔ B = R A

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = A → x 𝖨𝗆𝖺𝗀𝖾 R y ↔ A 𝖨𝗆𝖺𝗀𝖾 R y
2 imaeq2 ⊢ x = A → R x = R A
3 2 eqeq2d ⊢ x = A → y = R x ↔ y = R A
4 1 3 bibi12d ⊢ x = A → x 𝖨𝗆𝖺𝗀𝖾 R y ↔ y = R x ↔ A 𝖨𝗆𝖺𝗀𝖾 R y ↔ y = R A
5 breq2 ⊢ y = B → A 𝖨𝗆𝖺𝗀𝖾 R y ↔ A 𝖨𝗆𝖺𝗀𝖾 R B
6 eqeq1 ⊢ y = B → y = R A ↔ B = R A
7 5 6 bibi12d ⊢ y = B → A 𝖨𝗆𝖺𝗀𝖾 R y ↔ y = R A ↔ A 𝖨𝗆𝖺𝗀𝖾 R B ↔ B = R A
8 vex ⊢ x ∈ V
9 vex ⊢ y ∈ V
10 8 9 brimage ⊢ x 𝖨𝗆𝖺𝗀𝖾 R y ↔ y = R x
11 4 7 10 vtocl2g ⊢ A ∈ V ∧ B ∈ W → A 𝖨𝗆𝖺𝗀𝖾 R B ↔ B = R A