Metamath Proof Explorer

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 ⊢p=ab→ψ↔χ
Assertion reu3op ⊢∃!p∈X×Yψ↔∃a∈X∃b∈Yχ∧∃x∈X∃y∈Y∀a∈X∀b∈Yχ→xy=ab

Proof

Step Hyp Ref Expression
1 reu3op.a ⊢p=ab→ψ↔χ
2 reu3 ⊢∃!p∈X×Yψ↔∃p∈X×Yψ∧∃q∈X×Y∀p∈X×Yψ→p=q
3 1 rexxp ⊢∃p∈X×Yψ↔∃a∈X∃b∈Yχ
4 eqeq2 ⊢q=xy→p=q↔p=xy
5 4 imbi2d ⊢q=xy→ψ→p=q↔ψ→p=xy
6 5 ralbidv ⊢q=xy→∀p∈X×Yψ→p=q↔∀p∈X×Yψ→p=xy
7 6 rexxp ⊢∃q∈X×Y∀p∈X×Yψ→p=q↔∃x∈X∃y∈Y∀p∈X×Yψ→p=xy
8 eqeq1 ⊢p=ab→p=xy↔ab=xy
9 1 8 imbi12d ⊢p=ab→ψ→p=xy↔χ→ab=xy
10 9 ralxp ⊢∀p∈X×Yψ→p=xy↔∀a∈X∀b∈Yχ→ab=xy
11 eqcom ⊢ab=xy↔xy=ab
12 11 a1i ⊢x∈X∧y∈Y∧a∈X∧b∈Y→ab=xy↔xy=ab
13 12 imbi2d ⊢x∈X∧y∈Y∧a∈X∧b∈Y→χ→ab=xy↔χ→xy=ab
14 13 2ralbidva ⊢x∈X∧y∈Y→∀a∈X∀b∈Yχ→ab=xy↔∀a∈X∀b∈Yχ→xy=ab
15 10 14 bitrid ⊢x∈X∧y∈Y→∀p∈X×Yψ→p=xy↔∀a∈X∀b∈Yχ→xy=ab
16 15 2rexbiia ⊢∃x∈X∃y∈Y∀p∈X×Yψ→p=xy↔∃x∈X∃y∈Y∀a∈X∀b∈Yχ→xy=ab
17 7 16 bitri ⊢∃q∈X×Y∀p∈X×Yψ→p=q↔∃x∈X∃y∈Y∀a∈X∀b∈Yχ→xy=ab
18 3 17 anbi12i ⊢∃p∈X×Yψ∧∃q∈X×Y∀p∈X×Yψ→p=q↔∃a∈X∃b∈Yχ∧∃x∈X∃y∈Y∀a∈X∀b∈Yχ→xy=ab
19 2 18 bitri ⊢∃!p∈X×Yψ↔∃a∈X∃b∈Yχ∧∃x∈X∃y∈Y∀a∈X∀b∈Yχ→xy=ab