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	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
2	1	anbi1d	⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
3	2	3exbidv	⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
4		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
5	3 4	elab2g	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
6	5	ibi	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
7		id	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
8		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
9		vex	⊢ 𝑧 ∈ V
10	8 9	op1std	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ 𝐴 ) = ⟨ 𝑥 , 𝑦 ⟩ )
11	10	fveq2d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ ( 1st ‘ 𝐴 ) ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
12		vex	⊢ 𝑥 ∈ V
13		vex	⊢ 𝑦 ∈ V
14	12 13	op1st	⊢ ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
15	11 14	eqtr2di	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) )
16	10	fveq2d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ ( 1st ‘ 𝐴 ) ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17	12 13	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
18	16 17	eqtr2di	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) )
19	15 18	opeq12d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ )
20	8 9	op2ndd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑧 )
21	20	eqcomd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑧 = ( 2nd ‘ 𝐴 ) )
22	19 21	opeq12d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )
23	7 22	eqtrd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )
24	23	adantr	⊢ ( ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )
25	24	exlimiv	⊢ ( ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )
26	25	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )
27	6 26	syl	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝐴 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝐴 ) ) , ( 2nd ‘ ( 1st ‘ 𝐴 ) ) ⟩ , ( 2nd ‘ 𝐴 ) ⟩ )