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

Metamath Proof Explorer

Theorem brdomaing

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

Ref Expression
Assertion brdomaing ⊢ A ∈ V ∧ B ∈ W → A 𝖣𝗈𝗆𝖺𝗂𝗇 B ↔ B = dom ⁡ A

Proof

Step Hyp Ref Expression
1 breq1 ⊢ a = A → a 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ A 𝖣𝗈𝗆𝖺𝗂𝗇 b
2 dmeq ⊢ a = A → dom ⁡ a = dom ⁡ A
3 2 eqeq2d ⊢ a = A → b = dom ⁡ a ↔ b = dom ⁡ A
4 1 3 bibi12d ⊢ a = A → a 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ b = dom ⁡ a ↔ A 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ b = dom ⁡ A
5 breq2 ⊢ b = B → A 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ A 𝖣𝗈𝗆𝖺𝗂𝗇 B
6 eqeq1 ⊢ b = B → b = dom ⁡ A ↔ B = dom ⁡ A
7 5 6 bibi12d ⊢ b = B → A 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ b = dom ⁡ A ↔ A 𝖣𝗈𝗆𝖺𝗂𝗇 B ↔ B = dom ⁡ A
8 vex ⊢ a ∈ V
9 vex ⊢ b ∈ V
10 8 9 brdomain ⊢ a 𝖣𝗈𝗆𝖺𝗂𝗇 b ↔ b = dom ⁡ a
11 4 7 10 vtocl2g ⊢ A ∈ V ∧ B ∈ W → A 𝖣𝗈𝗆𝖺𝗂𝗇 B ↔ B = dom ⁡ A