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