Theorem reu3op

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023)

	Ref	Expression
Hypothesis	reu3op.a	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
Assertion	reu3op	⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		reu3op.a	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
2		reu3	⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ∧ ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ) )
3	1	rexxp	⊢ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 )
4		eqeq2	⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 = 𝑞 ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
5	4	imbi2d	⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝜓 → 𝑝 = 𝑞 ) ↔ ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
6	5	ralbidv	⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
7	6	rexxp	⊢ ( ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
8		eqeq1	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
9	1 8	imbi12d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
10	9	ralxp	⊢ ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
11		eqcom	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
12	11	a1i	⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
13	12	imbi2d	⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
14	13	2ralbidva	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
15	10 14	bitrid	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
16	15	2rexbiia	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
17	7 16	bitri	⊢ ( ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
18	3 17	anbi12i	⊢ ( ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ∧ ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ) ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
19	2 18	bitri	⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )