Theorem releldm2

Description: Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013)

	Ref	Expression
Assertion	releldm2	|- ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( B e. dom A -> B e. _V )
2	1	anim2i	|- ( ( Rel A /\ B e. dom A ) -> ( Rel A /\ B e. _V ) )
3		id	|- ( ( 1st ` x ) = B -> ( 1st ` x ) = B )
4		fvex	|- ( 1st ` x ) e. _V
5	3 4	eqeltrrdi	|- ( ( 1st ` x ) = B -> B e. _V )
6	5	rexlimivw	|- ( E. x e. A ( 1st ` x ) = B -> B e. _V )
7	6	anim2i	|- ( ( Rel A /\ E. x e. A ( 1st ` x ) = B ) -> ( Rel A /\ B e. _V ) )
8		eldm2g	|- ( B e. _V -> ( B e. dom A <-> E. y <. B , y >. e. A ) )
9	8	adantl	|- ( ( Rel A /\ B e. _V ) -> ( B e. dom A <-> E. y <. B , y >. e. A ) )
10		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
11		ssel	|- ( A C_ ( _V X. _V ) -> ( x e. A -> x e. ( _V X. _V ) ) )
12	10 11	sylbi	|- ( Rel A -> ( x e. A -> x e. ( _V X. _V ) ) )
13	12	imp	|- ( ( Rel A /\ x e. A ) -> x e. ( _V X. _V ) )
14		op1steq	|- ( x e. ( _V X. _V ) -> ( ( 1st ` x ) = B <-> E. y x = <. B , y >. ) )
15	13 14	syl	|- ( ( Rel A /\ x e. A ) -> ( ( 1st ` x ) = B <-> E. y x = <. B , y >. ) )
16	15	rexbidva	|- ( Rel A -> ( E. x e. A ( 1st ` x ) = B <-> E. x e. A E. y x = <. B , y >. ) )
17	16	adantr	|- ( ( Rel A /\ B e. _V ) -> ( E. x e. A ( 1st ` x ) = B <-> E. x e. A E. y x = <. B , y >. ) )
18		rexcom4	|- ( E. x e. A E. y x = <. B , y >. <-> E. y E. x e. A x = <. B , y >. )
19		risset	|- ( <. B , y >. e. A <-> E. x e. A x = <. B , y >. )
20	19	exbii	|- ( E. y <. B , y >. e. A <-> E. y E. x e. A x = <. B , y >. )
21	18 20	bitr4i	|- ( E. x e. A E. y x = <. B , y >. <-> E. y <. B , y >. e. A )
22	17 21	bitrdi	|- ( ( Rel A /\ B e. _V ) -> ( E. x e. A ( 1st ` x ) = B <-> E. y <. B , y >. e. A ) )
23	9 22	bitr4d	|- ( ( Rel A /\ B e. _V ) -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )
24	2 7 23	pm5.21nd	|- ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )