Metamath Proof Explorer

Theorem iotan0

Description: Representation of "the unique element such that ph " with a class expression A which is not the empty set (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024) Remove sethood antecedent. (Revised by Eric Schmidt, 17-Oct-2026)

Ref Expression
Hypothesis iotan0.1 ⊢ x = A → φ ↔ ψ
Assertion iotan0 ⊢ A ≠ ∅ ∧ A = ι x | φ → ψ

Proof

Step Hyp Ref Expression
1 iotan0.1 ⊢ x = A → φ ↔ ψ
2 pm13.18 ⊢ A = ι x | φ ∧ A ≠ ∅ → ι x | φ ≠ ∅
3 2 expcom ⊢ A ≠ ∅ → A = ι x | φ → ι x | φ ≠ ∅
4 iotanul ⊢ ¬ ∃! x φ → ι x | φ = ∅
5 4 necon1ai ⊢ ι x | φ ≠ ∅ → ∃! x φ
6 3 5 syl6 ⊢ A ≠ ∅ → A = ι x | φ → ∃! x φ
7 6 imp ⊢ A ≠ ∅ ∧ A = ι x | φ → ∃! x φ
8 iotaex ⊢ ι x | φ ∈ V
9 eleq1 ⊢ A = ι x | φ → A ∈ V ↔ ι x | φ ∈ V
10 8 9 mpbiri ⊢ A = ι x | φ → A ∈ V
11 eqcom ⊢ A = ι x | φ ↔ ι x | φ = A
12 1 iota2 ⊢ A ∈ V ∧ ∃! x φ → ψ ↔ ι x | φ = A
13 12 biimprd ⊢ A ∈ V ∧ ∃! x φ → ι x | φ = A → ψ
14 11 13 biimtrid ⊢ A ∈ V ∧ ∃! x φ → A = ι x | φ → ψ
15 14 impancom ⊢ A ∈ V ∧ A = ι x | φ → ∃! x φ → ψ
16 10 15 mpancom ⊢ A = ι x | φ → ∃! x φ → ψ
17 16 adantl ⊢ A ≠ ∅ ∧ A = ι x | φ → ∃! x φ → ψ
18 7 17 mpd ⊢ A ≠ ∅ ∧ A = ι x | φ → ψ