This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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)

Ref Expression
Hypothesis iotan0.1 ⊢ x = A → φ ↔ ψ
Assertion iotan0 ⊢ A ∈ V ∧ 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 a1i ⊢ A ∈ V → A ≠ ∅ → A = ι x | φ → ∃! x φ
8 7 3imp ⊢ A ∈ V ∧ A ≠ ∅ ∧ A = ι x | φ → ∃! x φ
9 eqcom ⊢ A = ι x | φ ↔ ι x | φ = A
10 1 iota2 ⊢ A ∈ V ∧ ∃! x φ → ψ ↔ ι x | φ = A
11 10 biimprd ⊢ A ∈ V ∧ ∃! x φ → ι x | φ = A → ψ
12 9 11 biimtrid ⊢ A ∈ V ∧ ∃! x φ → A = ι x | φ → ψ
13 12 impancom ⊢ A ∈ V ∧ A = ι x | φ → ∃! x φ → ψ
14 13 3adant2 ⊢ A ∈ V ∧ A ≠ ∅ ∧ A = ι x | φ → ∃! x φ → ψ
15 8 14 mpd ⊢ A ∈ V ∧ A ≠ ∅ ∧ A = ι x | φ → ψ