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 𝐴 ) )