Description: Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | opreu2reu1.a | ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜒 ↔ 𝜑 ) ) | |
| Assertion | opreu2reu1 | ⊢ ( ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opreu2reu1.a | ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜒 ↔ 𝜑 ) ) | |
| 2 | df-2reu | ⊢ ( ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 3 | 1 | opreu2reurex | ⊢ ( ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜒 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) |
| 4 | 2 3 | bitr4i | ⊢ ( ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜒 ) |