Metamath Proof Explorer

Theorem breldmg

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007)

Ref Expression
Assertion breldmg 
|- ( ( A e. C /\ B e. D /\ A R B ) -> A e. dom R )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = B -> ( A R x <-> A R B ) )
2 1 spcegv 
 |-  ( B e. D -> ( A R B -> E. x A R x ) )
3 2 imp 
 |-  ( ( B e. D /\ A R B ) -> E. x A R x )
4 eldmg 
 |-  ( A e. C -> ( A e. dom R <-> E. x A R x ) )
5 3 4 syl5ibr 
 |-  ( A e. C -> ( ( B e. D /\ A R B ) -> A e. dom R ) )
6 5 3impib 
 |-  ( ( A e. C /\ B e. D /\ A R B ) -> A e. dom R )