Theorem brabg2

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

	Ref	Expression
Hypotheses	brabg2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	brabg2.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
	brabg2.3	$$⊢R=\left\{⟨x,y⟩|\phi \right\}$$
	brabg2.4	$$⊢\chi \to A\in C$$
Assertion	brabg2	$$⊢B\in D\to \left(ARB\leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		brabg2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		brabg2.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3		brabg2.3	$$⊢R=\left\{⟨x,y⟩|\phi \right\}$$
4		brabg2.4	$$⊢\chi \to A\in C$$
5	3	relopabiv	$$⊢\mathrm{Rel}R$$
6	5	brrelex1i	$$⊢ARB\to A\in \mathrm{V}$$
7	1 2 3	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in D\right)\to \left(ARB\leftrightarrow \chi \right)$$
8	7	biimpd	$$⊢\left(A\in \mathrm{V}\wedge B\in D\right)\to \left(ARB\to \chi \right)$$
9	8	ex	$$⊢A\in \mathrm{V}\to \left(B\in D\to \left(ARB\to \chi \right)\right)$$
10	9	com3l	$$⊢B\in D\to \left(ARB\to \left(A\in \mathrm{V}\to \chi \right)\right)$$
11	6 10	mpdi	$$⊢B\in D\to \left(ARB\to \chi \right)$$
12	1 2 3	brabg	$$⊢\left(A\in C\wedge B\in D\right)\to \left(ARB\leftrightarrow \chi \right)$$
13	12	exbiri	$$⊢A\in C\to \left(B\in D\to \left(\chi \to ARB\right)\right)$$
14	13	com3l	$$⊢B\in D\to \left(\chi \to \left(A\in C\to ARB\right)\right)$$
15	4 14	mpdi	$$⊢B\in D\to \left(\chi \to ARB\right)$$
16	11 15	impbid	$$⊢B\in D\to \left(ARB\leftrightarrow \chi \right)$$