Metamath Proof Explorer

Theorem brdomaing

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

Ref Expression
Assertion brdomaing 
|- ( ( A e. V /\ B e. W ) -> ( A Domain B <-> B = dom A ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( a = A -> ( a Domain b <-> A Domain 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 Domain b <-> b = dom a ) <-> ( A Domain b <-> b = dom A ) ) )
5 breq2 
 |-  ( b = B -> ( A Domain b <-> A Domain B ) )
6 eqeq1 
 |-  ( b = B -> ( b = dom A <-> B = dom A ) )
7 5 6 bibi12d 
 |-  ( b = B -> ( ( A Domain b <-> b = dom A ) <-> ( A Domain B <-> B = dom A ) ) )
8 vex 
 |-  a e. _V
9 vex 
 |-  b e. _V
10 8 9 brdomain 
 |-  ( a Domain b <-> b = dom a )
11 4 7 10 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( A Domain B <-> B = dom A ) )