Metamath Proof Explorer

Theorem brrangeg

Description: Closed form of brrange . (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion brrangeg ⊢ A ∈ V ∧ B ∈ W → A 𝖱𝖺𝗇𝗀𝖾 B ↔ B = ran ⁡ A

Proof

Step Hyp Ref Expression
1 breq1 ⊢ a = A → a 𝖱𝖺𝗇𝗀𝖾 b ↔ A 𝖱𝖺𝗇𝗀𝖾 b
2 rneq ⊢ a = A → ran ⁡ a = ran ⁡ A
3 2 eqeq2d ⊢ a = A → b = ran ⁡ a ↔ b = ran ⁡ A
4 1 3 bibi12d ⊢ a = A → a 𝖱𝖺𝗇𝗀𝖾 b ↔ b = ran ⁡ a ↔ A 𝖱𝖺𝗇𝗀𝖾 b ↔ b = ran ⁡ A
5 breq2 ⊢ b = B → A 𝖱𝖺𝗇𝗀𝖾 b ↔ A 𝖱𝖺𝗇𝗀𝖾 B
6 eqeq1 ⊢ b = B → b = ran ⁡ A ↔ B = ran ⁡ A
7 5 6 bibi12d ⊢ b = B → A 𝖱𝖺𝗇𝗀𝖾 b ↔ b = ran ⁡ A ↔ A 𝖱𝖺𝗇𝗀𝖾 B ↔ B = ran ⁡ A
8 vex ⊢ a ∈ V
9 vex ⊢ b ∈ V
10 8 9 brrange ⊢ a 𝖱𝖺𝗇𝗀𝖾 b ↔ b = ran ⁡ a
11 4 7 10 vtocl2g ⊢ A ∈ V ∧ B ∈ W → A 𝖱𝖺𝗇𝗀𝖾 B ↔ B = ran ⁡ A