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 simpr ⊢ φ ∧ ∃! x ∈ A ψ → ∃! x ∈ A ψ
8 df-reu ⊢ ∃! x ∈ A ψ ↔ ∃! x x ∈ A ∧ ψ
9 7 8 sylib ⊢ φ ∧ ∃! x ∈ A ψ → ∃! x x ∈ A ∧ ψ
10 simpr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x = B
11 6 adantr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → B ∈ A
12 10 11 eqeltrd ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x ∈ A
13 12 biantrurd ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → ψ ↔ x ∈ A ∧ ψ
14 5 adantlr ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → ψ ↔ χ
15 13 14 bitr3d ⊢ φ ∧ ∃! x ∈ A ψ ∧ x = B → x ∈ A ∧ ψ ↔ χ
16 nfreu1 ⊢ Ⅎ x ∃! x ∈ A ψ
17 1 16 nfan ⊢ Ⅎ x φ ∧ ∃! x ∈ A ψ
18 3 adantr ⊢ φ ∧ ∃! x ∈ A ψ → Ⅎ x χ
19 2 adantr ⊢ φ ∧ ∃! x ∈ A ψ → Ⅎ _ x B
20 6 9 15 17 18 19 iota2df ⊢ φ ∧ ∃! x ∈ A ψ → χ ↔ ι x | x ∈ A ∧ ψ = B
21 df-riota ⊢ ι x ∈ A | ψ = ι x | x ∈ A ∧ ψ
22 21 eqeq1i ⊢ ι x ∈ A | ψ = B ↔ ι x | x ∈ A ∧ ψ = B
23 20 22 bitr4di ⊢ φ ∧ ∃! x ∈ A ψ → χ ↔ ι x ∈ A | ψ = B