Metamath Proof Explorer


Theorem reu8

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006)

Ref Expression
Hypothesis rmo4.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion reu8 ( ∃! 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐴 ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 rmo4.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 1 cbvreuvw ( ∃! 𝑥𝐴 𝜑 ↔ ∃! 𝑦𝐴 𝜓 )
3 reu6 ( ∃! 𝑦𝐴 𝜓 ↔ ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) )
4 dfbi2 ( ( 𝜓𝑦 = 𝑥 ) ↔ ( ( 𝜓𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥𝜓 ) ) )
5 4 ralbii ( ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ↔ ∀ 𝑦𝐴 ( ( 𝜓𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥𝜓 ) ) )
6 r19.26 ( ∀ 𝑦𝐴 ( ( 𝜓𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥𝜓 ) ) ↔ ( ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ∧ ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) ) )
7 ancom ( ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ∧ 𝜑 ) )
8 equcom ( 𝑥 = 𝑦𝑦 = 𝑥 )
9 8 imbi2i ( ( 𝜓𝑥 = 𝑦 ) ↔ ( 𝜓𝑦 = 𝑥 ) )
10 9 ralbii ( ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ↔ ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) )
11 10 a1i ( 𝑥𝐴 → ( ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ↔ ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ) )
12 biimt ( 𝑥𝐴 → ( 𝜑 ↔ ( 𝑥𝐴𝜑 ) ) )
13 df-ral ( ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) ↔ ∀ 𝑦 ( 𝑦𝐴 → ( 𝑦 = 𝑥𝜓 ) ) )
14 bi2.04 ( ( 𝑦𝐴 → ( 𝑦 = 𝑥𝜓 ) ) ↔ ( 𝑦 = 𝑥 → ( 𝑦𝐴𝜓 ) ) )
15 14 albii ( ∀ 𝑦 ( 𝑦𝐴 → ( 𝑦 = 𝑥𝜓 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑦𝐴𝜓 ) ) )
16 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐴𝑦𝐴 ) )
17 16 1 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑦𝐴𝜓 ) ) )
18 17 bicomd ( 𝑥 = 𝑦 → ( ( 𝑦𝐴𝜓 ) ↔ ( 𝑥𝐴𝜑 ) ) )
19 18 equcoms ( 𝑦 = 𝑥 → ( ( 𝑦𝐴𝜓 ) ↔ ( 𝑥𝐴𝜑 ) ) )
20 19 equsalvw ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑦𝐴𝜓 ) ) ↔ ( 𝑥𝐴𝜑 ) )
21 13 15 20 3bitrri ( ( 𝑥𝐴𝜑 ) ↔ ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) )
22 12 21 bitrdi ( 𝑥𝐴 → ( 𝜑 ↔ ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) ) )
23 11 22 anbi12d ( 𝑥𝐴 → ( ( ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ∧ 𝜑 ) ↔ ( ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ∧ ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) ) ) )
24 7 23 syl5bb ( 𝑥𝐴 → ( ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ∧ ∀ 𝑦𝐴 ( 𝑦 = 𝑥𝜓 ) ) ) )
25 6 24 bitr4id ( 𝑥𝐴 → ( ∀ 𝑦𝐴 ( ( 𝜓𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥𝜓 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) ) )
26 5 25 syl5bb ( 𝑥𝐴 → ( ∀ 𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ↔ ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) ) )
27 26 rexbiia ( ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑦 = 𝑥 ) ↔ ∃ 𝑥𝐴 ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )
28 2 3 27 3bitri ( ∃! 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐴 ( 𝜑 ∧ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )