Theorem opelopab3

Description: Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011)

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

Proof

Step	Hyp	Ref	Expression
1		opelopab3.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		opelopab3.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3		opelopab3.3	$$⊢\chi \to A\in C$$
4		elopaelxp	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\to ⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
5		opelxp1	$$⊢⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to A\in \mathrm{V}$$
6	4 5	syl	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\to A\in \mathrm{V}$$
7	6	anim1i	$$⊢\left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\wedge B\in D\right)\to \left(A\in \mathrm{V}\wedge B\in D\right)$$
8	7	ancoms	$$⊢\left(B\in D\wedge ⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\right)\to \left(A\in \mathrm{V}\wedge B\in D\right)$$
9	3	elexd	$$⊢\chi \to A\in \mathrm{V}$$
10	9	anim1i	$$⊢\left(\chi \wedge B\in D\right)\to \left(A\in \mathrm{V}\wedge B\in D\right)$$
11	10	ancoms	$$⊢\left(B\in D\wedge \chi \right)\to \left(A\in \mathrm{V}\wedge B\in D\right)$$
12	1 2	opelopabg	$$⊢\left(A\in \mathrm{V}\wedge B\in D\right)\to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi \right)$$
13	8 11 12	pm5.21nd	$$⊢B\in D\to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi \right)$$