Theorem elopabi

Description: A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006)

	Ref	Expression
Hypotheses	elopabi.1	$$⊢x=1^{st}\left(A\right)\to \left(\phi \leftrightarrow \psi \right)$$
	elopabi.2	$$⊢y=2^{nd}\left(A\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	elopabi	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		elopabi.1	$$⊢x=1^{st}\left(A\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		elopabi.2	$$⊢y=2^{nd}\left(A\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		relopab	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$
4		1st2nd	$$⊢\left(\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}\wedge A\in \left\{⟨x,y⟩|\phi \right\}\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
5	3 4	mpan	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
6		id	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to A\in \left\{⟨x,y⟩|\phi \right\}$$
7	5 6	eqeltrrd	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \left\{⟨x,y⟩|\phi \right\}$$
8		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
9		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
10	8 9 1 2	opelopab	$$⊢⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi$$
11	7 10	sylib	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to \chi$$