Theorem opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

	Ref	Expression
Hypothesis	opreuopreu.a	⊢ ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) → ( 𝜓 ↔ 𝜑 ) )
Assertion	opreuopreu	⊢ ( ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		opreuopreu.a	⊢ ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) → ( 𝜓 ↔ 𝜑 ) )
2		elxpi	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
3		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ )
4		vex	⊢ 𝑎 ∈ V
5		vex	⊢ 𝑏 ∈ V
6	4 5	op1st	⊢ ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑎
7	6	eqcomi	⊢ 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ )
8	4 5	op2nd	⊢ ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑏
9	8	eqcomi	⊢ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ )
10	7 9	pm3.2i	⊢ ( 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
11		fveq2	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑝 ) = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
12	11	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑎 = ( 1st ‘ 𝑝 ) ↔ 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
13		fveq2	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
14	13	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑏 = ( 2nd ‘ 𝑝 ) ↔ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
15	12 14	anbi12d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) ↔ ( 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
16	10 15	mpbiri	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) )
17	16 1	syl	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜑 ) )
18	17	biimprd	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 → 𝜓 ) )
19	18	adantr	⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝜑 → 𝜓 ) )
20	19	impcom	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → 𝜓 )
21	3 20	jca	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )
22	21	ex	⊢ ( 𝜑 → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
23	22	2eximdv	⊢ ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
24	2 23	syl5com	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( 𝜑 → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
25	17	biimpa	⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 )
26	25	a1i	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 ) )
27	26	exlimdvv	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 ) )
28	24 27	impbid	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( 𝜑 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
29	28	reubiia	⊢ ( ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )