This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) )