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 ⊢φ→Ⅎ_xB
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 ⊢φ→Ⅎ_xB
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ψ↔∃!xx∈A∧ψ
9 7 8 sylib ⊢φ∧∃!x∈Aψ→∃!xx∈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ψ→Ⅎ_xB
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