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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 Domain 𝐵 ↔ 𝐵 = dom 𝐴 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 Domain 𝑏 ↔ 𝐴 Domain 𝑏 ) )
2 dmeq ⊢ ( 𝑎 = 𝐴 → dom 𝑎 = dom 𝐴 )
3 2 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑏 = dom 𝑎 ↔ 𝑏 = dom 𝐴 ) )
4 1 3 bibi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 Domain 𝑏 ↔ 𝑏 = dom 𝑎 ) ↔ ( 𝐴 Domain 𝑏 ↔ 𝑏 = dom 𝐴 ) ) )
5 breq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 Domain 𝑏 ↔ 𝐴 Domain 𝐵 ) )
6 eqeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 = dom 𝐴 ↔ 𝐵 = dom 𝐴 ) )
7 5 6 bibi12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 Domain 𝑏 ↔ 𝑏 = dom 𝐴 ) ↔ ( 𝐴 Domain 𝐵 ↔ 𝐵 = dom 𝐴 ) ) )
8 vex ⊢ 𝑎 ∈ V
9 vex ⊢ 𝑏 ∈ V
10 8 9 brdomain ⊢ ( 𝑎 Domain 𝑏 ↔ 𝑏 = dom 𝑎 )
11 4 7 10 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 Domain 𝐵 ↔ 𝐵 = dom 𝐴 ) )