Theorem eloprab1st2nd

Description: Reconstruction of a nested ordered pair in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Assertion	eloprab1st2nd	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢w=A\to \left(w=⟨⟨x,y⟩,z⟩\leftrightarrow A=⟨⟨x,y⟩,z⟩\right)$$
2	1	anbi1d	$$⊢w=A\to \left(\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\leftrightarrow \left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
3	2	3exbidv	$$⊢w=A\to \left(\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
4		df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
5	3 4	elab2g	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \left(A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
6	5	ibi	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
7		id	$$⊢A=⟨⟨x,y⟩,z⟩\to A=⟨⟨x,y⟩,z⟩$$
8		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
9		vex	$$⊢z\in \mathrm{V}$$
10	8 9	op1std	$$⊢A=⟨⟨x,y⟩,z⟩\to 1^{st}\left(A\right)=⟨x,y⟩$$
11	10	fveq2d	$$⊢A=⟨⟨x,y⟩,z⟩\to 1^{st}\left(1^{st}\left(A\right)\right)=1^{st}\left(⟨x,y⟩\right)$$
12		vex	$$⊢x\in \mathrm{V}$$
13		vex	$$⊢y\in \mathrm{V}$$
14	12 13	op1st	$$⊢1^{st}\left(⟨x,y⟩\right)=x$$
15	11 14	eqtr2di	$$⊢A=⟨⟨x,y⟩,z⟩\to x=1^{st}\left(1^{st}\left(A\right)\right)$$
16	10	fveq2d	$$⊢A=⟨⟨x,y⟩,z⟩\to 2^{nd}\left(1^{st}\left(A\right)\right)=2^{nd}\left(⟨x,y⟩\right)$$
17	12 13	op2nd	$$⊢2^{nd}\left(⟨x,y⟩\right)=y$$
18	16 17	eqtr2di	$$⊢A=⟨⟨x,y⟩,z⟩\to y=2^{nd}\left(1^{st}\left(A\right)\right)$$
19	15 18	opeq12d	$$⊢A=⟨⟨x,y⟩,z⟩\to ⟨x,y⟩=⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩$$
20	8 9	op2ndd	$$⊢A=⟨⟨x,y⟩,z⟩\to 2^{nd}\left(A\right)=z$$
21	20	eqcomd	$$⊢A=⟨⟨x,y⟩,z⟩\to z=2^{nd}\left(A\right)$$
22	19 21	opeq12d	$$⊢A=⟨⟨x,y⟩,z⟩\to ⟨⟨x,y⟩,z⟩=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
23	7 22	eqtrd	$$⊢A=⟨⟨x,y⟩,z⟩\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
24	23	adantr	$$⊢\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
25	24	exlimiv	$$⊢\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
26	25	exlimivv	$$⊢\exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
27	6 26	syl	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$