Metamath Proof Explorer

Theorem riota2df

Description: A deduction version of riota2f . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riota2df.1 ⊢ Ⅎ x φ
riota2df.2 ⊢ φ → Ⅎ _ x B
riota2df.3 ⊢ φ → Ⅎ x χ
riota2df.4 ⊢ φ → B ∈ A
riota2df.5 ⊢ φ ∧ x = B → ψ ↔ χ
Assertion riota2df ⊢ φ ∧ ∃! x ∈ A ψ → χ ↔ ι x ∈ A | ψ = B

Proof

Step Hyp Ref Expression
1 riota2df.1 ⊢ Ⅎ x φ
2 riota2df.2 ⊢ φ → Ⅎ _ x B
3 riota2df.3 ⊢ φ → Ⅎ x χ
4 riota2df.4 ⊢ φ → B ∈ A
5 riota2df.5 ⊢ φ ∧ x = B → ψ ↔ χ
6 4 adantr ⊢ φ ∧ ∃! x ∈ A ψ → B ∈ A
7 df-reu ⊢ ∃! x ∈ A ψ ↔ ∃! x x ∈ A ∧ ψ
8 7 bilani ⊢ φ ∧ ∃! x ∈ A ψ → ∃! x x ∈ A ∧ ψ
9 simpr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x = B
10 6 adantr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → B ∈ A
11 9 10 eqeltrd ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x ∈ A
12 11 biantrurd ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → ψ ↔ x ∈ A ∧ ψ
13 5 adantlr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → ψ ↔ χ
14 12 13 bitr3d ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x ∈ A ∧ ψ ↔ χ
15 nfreu1 ⊢ Ⅎ x ∃! x ∈ A ψ
16 1 15 nfan ⊢ Ⅎ x φ ∧ ∃! x ∈ A ψ
17 3 adantr ⊢ φ ∧ ∃! x ∈ A ψ → Ⅎ x χ
18 2 adantr ⊢ φ ∧ ∃! x ∈ A ψ → Ⅎ _ x B
19 6 8 14 16 17 18 iota2df ⊢ φ ∧ ∃! x ∈ A ψ → χ ↔ ι x | x ∈ A ∧ ψ = B
20 df-riota ⊢ ι x ∈ A | ψ = ι x | x ∈ A ∧ ψ
21 20 eqeq1i ⊢ ι x ∈ A | ψ = B ↔ ι x | x ∈ A ∧ ψ = B
22 19 21 bitr4di ⊢ φ ∧ ∃! x ∈ A ψ → χ ↔ ι x ∈ A | ψ = B