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	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → 𝜓 ) )
13	12	impancom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
14	13	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
15	8 14	mpd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → 𝜓 )