Theorem elreldm

Description: The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb ). (Contributed by NM, 28-Jul-2004)

	Ref	Expression
Assertion	elreldm	|- ( ( Rel A /\ B e. A ) -> |^| |^| B e. dom A )

Proof

Step	Hyp	Ref	Expression
1		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
2		ssel	|- ( A C_ ( _V X. _V ) -> ( B e. A -> B e. ( _V X. _V ) ) )
3	1 2	sylbi	|- ( Rel A -> ( B e. A -> B e. ( _V X. _V ) ) )
4		elvv	|- ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. )
5	3 4	syl6ib	|- ( Rel A -> ( B e. A -> E. x E. y B = <. x , y >. ) )
6		eleq1	|- ( B = <. x , y >. -> ( B e. A <-> <. x , y >. e. A ) )
7		vex	|- x e. _V
8		vex	|- y e. _V
9	7 8	opeldm	|- ( <. x , y >. e. A -> x e. dom A )
10	6 9	syl6bi	|- ( B = <. x , y >. -> ( B e. A -> x e. dom A ) )
11		inteq	|- ( B = <. x , y >. -> |^| B = |^| <. x , y >. )
12	11	inteqd	|- ( B = <. x , y >. -> |^| |^| B = |^| |^| <. x , y >. )
13	7 8	op1stb	|- |^| |^| <. x , y >. = x
14	12 13	eqtrdi	|- ( B = <. x , y >. -> |^| |^| B = x )
15	14	eleq1d	|- ( B = <. x , y >. -> ( |^| |^| B e. dom A <-> x e. dom A ) )
16	10 15	sylibrd	|- ( B = <. x , y >. -> ( B e. A -> |^| |^| B e. dom A ) )
17	16	exlimivv	|- ( E. x E. y B = <. x , y >. -> ( B e. A -> |^| |^| B e. dom A ) )
18	5 17	syli	|- ( Rel A -> ( B e. A -> |^| |^| B e. dom A ) )
19	18	imp	|- ( ( Rel A /\ B e. A ) -> |^| |^| B e. dom A )