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