Theorem aiotaexim

Description: Representation of "the unique element such that ph " with a class expression A which is a set (that means that "the unique element such that ph " exists). Analog to iotan0 which requires A to be nonempty instead of being a set. That gives a more natural statement, closer to statements like spcgv . (Proposed by BJ, 18-Oct-2026.) (Contributed by AV, 18-Oct-2026)

	Ref	Expression
Hypothesis	aiotaexim.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	aiotaexim	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = ( ℩' 𝑥 𝜑 ) ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		aiotaexim.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		dfaiota3	⊢ ( ℩' 𝑥 𝜑 ) = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V )
3	2	eqeq2i	⊢ ( 𝐴 = ( ℩' 𝑥 𝜑 ) ↔ 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) )
4		iftrue	⊢ ( ∃! 𝑥 𝜑 → if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) = ∩ { 𝑥 ∣ 𝜑 } )
5	4	eqeq2d	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) ↔ 𝐴 = ∩ { 𝑥 ∣ 𝜑 } ) )
6		iotain	⊢ ( ∃! 𝑥 𝜑 → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )
7	6	eqeq2d	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 = ∩ { 𝑥 ∣ 𝜑 } ↔ 𝐴 = ( ℩ 𝑥 𝜑 ) ) )
8		eqcom	⊢ ( 𝐴 = ( ℩ 𝑥 𝜑 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 )
9	1	iota2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )
10	9	biimprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃! 𝑥 𝜑 ) → ( ( ℩ 𝑥 𝜑 ) = 𝐴 → 𝜓 ) )
11	10	expcom	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 ∈ 𝑉 → ( ( ℩ 𝑥 𝜑 ) = 𝐴 → 𝜓 ) ) )
12	11	com23	⊢ ( ∃! 𝑥 𝜑 → ( ( ℩ 𝑥 𝜑 ) = 𝐴 → ( 𝐴 ∈ 𝑉 → 𝜓 ) ) )
13	8 12	biimtrid	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 = ( ℩ 𝑥 𝜑 ) → ( 𝐴 ∈ 𝑉 → 𝜓 ) ) )
14	7 13	sylbid	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 = ∩ { 𝑥 ∣ 𝜑 } → ( 𝐴 ∈ 𝑉 → 𝜓 ) ) )
15	5 14	sylbid	⊢ ( ∃! 𝑥 𝜑 → ( 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) → ( 𝐴 ∈ 𝑉 → 𝜓 ) ) )
16		iffalse	⊢ ( ¬ ∃! 𝑥 𝜑 → if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) = V )
17	16	eqeq2d	⊢ ( ¬ ∃! 𝑥 𝜑 → ( 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) ↔ 𝐴 = V ) )
18		nvelim	⊢ ( 𝐴 = V → ¬ 𝐴 ∈ 𝑉 )
19	18	pm2.21d	⊢ ( 𝐴 = V → ( 𝐴 ∈ 𝑉 → 𝜓 ) )
20	17 19	biimtrdi	⊢ ( ¬ ∃! 𝑥 𝜑 → ( 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) → ( 𝐴 ∈ 𝑉 → 𝜓 ) ) )
21	15 20	pm2.61i	⊢ ( 𝐴 = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) → ( 𝐴 ∈ 𝑉 → 𝜓 ) )
22	3 21	sylbi	⊢ ( 𝐴 = ( ℩' 𝑥 𝜑 ) → ( 𝐴 ∈ 𝑉 → 𝜓 ) )
23	22	impcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = ( ℩' 𝑥 𝜑 ) ) → 𝜓 )