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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
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	imp	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ∃! 𝑥 𝜑 )
8		iotaex	⊢ ( ℩ 𝑥 𝜑 ) ∈ V
9		eleq1	⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ( 𝐴 ∈ V ↔ ( ℩ 𝑥 𝜑 ) ∈ V ) )
10	8 9	mpbiri	⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) → 𝐴 ∈ V )
11		eqcom	⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 )
12	1	iota2	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )
13	12	biimprd	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → ( ( ℩ 𝑥 𝜑 ) = 𝐴 → 𝜓 ) )
14	11 13	biimtrid	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → 𝜓 ) )
15	14	impancom	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
16	10 15	mpancom	⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
17	16	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → ( ∃! 𝑥 𝜑 → 𝜓 ) )
18	7 17	mpd	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 = ( ℩ 𝑥 𝜑 ) ) → 𝜓 )