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 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion iotan0 ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → 𝜓 )

Proof

Step Hyp Ref Expression
1 iotan0.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 pm13.18 ⊢ ( ( 𝐴 = ( ℩ 𝑥 𝜑 ) ∧ 𝐴 ≠ ∅ ) → ( ℩ 𝑥 𝜑 ) ≠ ∅ )
3 2 expcom ⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ( ℩ 𝑥 𝜑 ) ≠ ∅ ) )
4 iotanul ⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )
5 4 necon1ai ⊢ ( ( ℩ 𝑥 𝜑 ) ≠ ∅ → ∃! 𝑥 𝜑 )
6 3 5 syl6 ⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ∃! 𝑥 𝜑 ) )
7 6 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ≠ ∅ → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ∃! 𝑥 𝜑 ) ) )
8 7 3imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ∃! 𝑥 𝜑 )
9 eqcom ⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 )
10 1 iota2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )
11 10 biimprd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( ( ℩ 𝑥 𝜑 ) = 𝐴 → 𝜓 ) )
12 9 11 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → 𝜓 ) )
13 12 impancom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
14 13 3adant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
15 8 14 mpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → 𝜓 )