Theorem brabg2

Description: Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	brabg2.1	|- ( x = A -> ( ph <-> ps ) )
	brabg2.2	|- ( y = B -> ( ps <-> ch ) )
	brabg2.3	|- R = { <. x , y >. | ph }
	brabg2.4	|- ( ch -> A e. C )
Assertion	brabg2	|- ( B e. D -> ( A R B <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		brabg2.1	|- ( x = A -> ( ph <-> ps ) )
2		brabg2.2	|- ( y = B -> ( ps <-> ch ) )
3		brabg2.3	|- R = { <. x , y >. | ph }
4		brabg2.4	|- ( ch -> A e. C )
5	3	relopabiv	|- Rel R
6	5	brrelex1i	|- ( A R B -> A e. _V )
7	1 2 3	brabg	|- ( ( A e. _V /\ B e. D ) -> ( A R B <-> ch ) )
8	7	biimpd	|- ( ( A e. _V /\ B e. D ) -> ( A R B -> ch ) )
9	8	ex	|- ( A e. _V -> ( B e. D -> ( A R B -> ch ) ) )
10	9	com3l	|- ( B e. D -> ( A R B -> ( A e. _V -> ch ) ) )
11	6 10	mpdi	|- ( B e. D -> ( A R B -> ch ) )
12	1 2 3	brabg	|- ( ( A e. C /\ B e. D ) -> ( A R B <-> ch ) )
13	12	exbiri	|- ( A e. C -> ( B e. D -> ( ch -> A R B ) ) )
14	13	com3l	|- ( B e. D -> ( ch -> ( A e. C -> A R B ) ) )
15	4 14	mpdi	|- ( B e. D -> ( ch -> A R B ) )
16	11 15	impbid	|- ( B e. D -> ( A R B <-> ch ) )