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 ⊢ A ∈ V → ∃! x ∈ A φ ↔ ι x ∈ A | φ ∈ A

Proof

Step Hyp Ref Expression
1 riotacl ⊢ ∃! x ∈ A φ → ι x ∈ A | φ ∈ A
2 undefnel2 ⊢ A ∈ V → ¬ Undef ⁡ A ∈ A
3 iffalse ⊢ ¬ ∃! x ∈ A φ → if ∃! x ∈ A φ ι x | x ∈ A ∧ φ Undef ⁡ x | x ∈ A = Undef ⁡ x | x ∈ A
4 ax-riotaBAD ⊢ ι x ∈ A | φ = if ∃! x ∈ A φ ι x | x ∈ A ∧ φ Undef ⁡ x | x ∈ A
5 abid1 ⊢ A = x | x ∈ A
6 5 fveq2i ⊢ Undef ⁡ A = Undef ⁡ x | x ∈ A
7 3 4 6 3eqtr4g ⊢ ¬ ∃! x ∈ A φ → ι x ∈ A | φ = Undef ⁡ A
8 7 eleq1d ⊢ ¬ ∃! x ∈ A φ → ι x ∈ A | φ ∈ A ↔ Undef ⁡ A ∈ A
9 8 notbid ⊢ ¬ ∃! x ∈ A φ → ¬ ι x ∈ A | φ ∈ A ↔ ¬ Undef ⁡ A ∈ A
10 2 9 syl5ibrcom ⊢ A ∈ V → ¬ ∃! x ∈ A φ → ¬ ι x ∈ A | φ ∈ A
11 10 con4d ⊢ A ∈ V → ι x ∈ A | φ ∈ A → ∃! x ∈ A φ
12 1 11 impbid2 ⊢ A ∈ V → ∃! x ∈ A φ ↔ ι x ∈ A | φ ∈ A