Theorem riotaclbgBAD

Description: Closure of restricted iota. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	riotaclbgBAD	⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		riotacl	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
2		undefnel2	⊢ ( 𝐴 ∈ 𝑉 → ¬ ( Undef ‘ 𝐴 ) ∈ 𝐴 )
3		iffalse	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → if ( ∃! 𝑥 ∈ 𝐴 𝜑 , ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) , ( Undef ‘ { 𝑥 ∣ 𝑥 ∈ 𝐴 } ) ) = ( Undef ‘ { 𝑥 ∣ 𝑥 ∈ 𝐴 } ) )
4		ax-riotaBAD	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = if ( ∃! 𝑥 ∈ 𝐴 𝜑 , ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) , ( Undef ‘ { 𝑥 ∣ 𝑥 ∈ 𝐴 } ) )
5		abid1	⊢ 𝐴 = { 𝑥 ∣ 𝑥 ∈ 𝐴 }
6	5	fveq2i	⊢ ( Undef ‘ 𝐴 ) = ( Undef ‘ { 𝑥 ∣ 𝑥 ∈ 𝐴 } )
7	3 4 6	3eqtr4g	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( Undef ‘ 𝐴 ) )
8	7	eleq1d	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ↔ ( Undef ‘ 𝐴 ) ∈ 𝐴 ) )
9	8	notbid	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ¬ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ↔ ¬ ( Undef ‘ 𝐴 ) ∈ 𝐴 ) )
10	2 9	syl5ibrcom	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ¬ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) )
11	10	con4d	⊢ ( 𝐴 ∈ 𝑉 → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
12	1 11	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) )