This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reu8nf

Description: Restricted uniqueness using implicit substitution. This version of reu8 uses a nonfreeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022)

Ref Expression
Hypotheses reu8nf.1 ⊢ Ⅎ 𝑥 𝜓
reu8nf.2 ⊢ Ⅎ 𝑥 𝜒
reu8nf.3 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
reu8nf.4 ⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
Assertion reu8nf ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 reu8nf.1 ⊢ Ⅎ 𝑥 𝜓
2 reu8nf.2 ⊢ Ⅎ 𝑥 𝜒
3 reu8nf.3 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
4 reu8nf.4 ⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
5 nfv ⊢ Ⅎ 𝑤 𝜑
6 5 2 3 cbvreuw ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑤 ∈ 𝐴 𝜒 )
7 4 reu8 ⊢ ( ∃! 𝑤 ∈ 𝐴 𝜒 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) )
8 nfcv ⊢ Ⅎ 𝑥 𝐴
9 nfv ⊢ Ⅎ 𝑥 𝑤 = 𝑦
10 1 9 nfim ⊢ Ⅎ 𝑥 ( 𝜓 → 𝑤 = 𝑦 )
11 8 10 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 )
12 2 11 nfan ⊢ Ⅎ 𝑥 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) )
13 nfv ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
14 3 bicomd ⊢ ( 𝑥 = 𝑤 → ( 𝜒 ↔ 𝜑 ) )
15 14 equcoms ⊢ ( 𝑤 = 𝑥 → ( 𝜒 ↔ 𝜑 ) )
16 equequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦 ↔ 𝑥 = 𝑦 ) )
17 16 imbi2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝜓 → 𝑤 = 𝑦 ) ↔ ( 𝜓 → 𝑥 = 𝑦 ) ) )
18 17 ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
19 15 18 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) )
20 12 13 19 cbvrexw ⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
21 6 7 20 3bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )