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 simpr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜓 )
8 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9 7 8 sylib ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
10 simpr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
11 6 adantr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝐴 )
12 10 11 eqeltrd ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
13 12 biantrurd ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
14 5 adantlr ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
15 13 14 bitr3d ⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝜒 ) )
16 nfreu1 ⊢ Ⅎ 𝑥 ∃! 𝑥 ∈ 𝐴 𝜓
17 1 16 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 )
18 3 adantr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝜒 )
19 2 adantr ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝐵 )
20 6 9 15 17 18 19 iota2df ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 ) )
21 df-riota ⊢ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
22 21 eqeq1i ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 )
23 20 22 bitr4di ⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )