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 ⊢ Ⅎ 𝑥 𝜑
riota2df.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
riota2df.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
riota2df.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
riota2df.5 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion riota2df ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 riota2df.1 ⊢ Ⅎ 𝑥 𝜑
2 riota2df.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3 riota2df.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
4 riota2df.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
5 riota2df.5 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
6 4 adantr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → 𝐵 ∈ 𝐴 )
7 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
8 7 bilani ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9 simpr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
10 6 adantr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝐴 )
11 9 10 eqeltrd ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
12 11 biantrurd ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
13 5 adantlr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
14 12 13 bitr3d ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝜒 ) )
15 nfreu1 ⊢ Ⅎ 𝑥 ∃! 𝑥 ∈ 𝐴 𝜓
16 1 15 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 )
17 3 adantr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝜒 )
18 2 adantr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝐵 )
19 6 8 14 16 17 18 iota2df ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 ) )
20 df-riota ⊢ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
21 20 eqeq1i ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 )
22 19 21 bitr4di ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )