Metamath Proof Explorer

Theorem reu6f

Description: Version of reu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BTernaryTau, 29-Sep-2026)

Ref Expression
Hypothesis reu6f.1 ⊢ Ⅎ 𝑦 𝜑
Assertion reu6f ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 reu6f.1 ⊢ Ⅎ 𝑦 𝜑
2 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
3 19.28v ⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
4 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
5 sbequ12 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
6 4 5 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
7 equequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑦 ) )
8 6 7 bibi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) ) )
9 equid ⊢ 𝑦 = 𝑦
10 9 tbt ⊢ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) )
11 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑦 ∈ 𝐴 )
12 10 11 sylbir ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) → 𝑦 ∈ 𝐴 )
13 8 12 biimtrdi ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐴 ) )
14 13 spimvw ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐴 )
15 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
16 15 bibi1d ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ) )
17 16 biimprcd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
18 17 sps ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
19 14 18 jca ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
20 19 axc4i ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
21 biimp ⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
22 21 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
23 22 impd ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
24 23 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
25 4 biimprcd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
27 26 imp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 ∈ 𝐴 )
28 simplr ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
29 simpr ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
30 biimpr ⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
31 28 29 30 syl6ci ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
32 27 31 jcai ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
33 32 ex ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
34 24 33 impbid ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
35 34 alimi ⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
36 20 35 impbii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
37 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
38 37 anbi2i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
39 3 36 38 3bitr4i ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
40 39 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
41 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
42 41 1 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
43 42 euf ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
44 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
45 40 43 44 3bitr4i ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
46 2 45 bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )