Metamath Proof Explorer


Theorem reu7

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

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

Proof

Step Hyp Ref Expression
1 rmo4.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 reu3 ( ∃! 𝑥𝐴 𝜑 ↔ ( ∃ 𝑥𝐴 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( 𝜑𝑥 = 𝑧 ) ) )
3 equequ1 ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧𝑦 = 𝑧 ) )
4 equcom ( 𝑦 = 𝑧𝑧 = 𝑦 )
5 3 4 bitrdi ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧𝑧 = 𝑦 ) )
6 1 5 imbi12d ( 𝑥 = 𝑦 → ( ( 𝜑𝑥 = 𝑧 ) ↔ ( 𝜓𝑧 = 𝑦 ) ) )
7 6 cbvralvw ( ∀ 𝑥𝐴 ( 𝜑𝑥 = 𝑧 ) ↔ ∀ 𝑦𝐴 ( 𝜓𝑧 = 𝑦 ) )
8 7 rexbii ( ∃ 𝑧𝐴𝑥𝐴 ( 𝜑𝑥 = 𝑧 ) ↔ ∃ 𝑧𝐴𝑦𝐴 ( 𝜓𝑧 = 𝑦 ) )
9 equequ1 ( 𝑧 = 𝑥 → ( 𝑧 = 𝑦𝑥 = 𝑦 ) )
10 9 imbi2d ( 𝑧 = 𝑥 → ( ( 𝜓𝑧 = 𝑦 ) ↔ ( 𝜓𝑥 = 𝑦 ) ) )
11 10 ralbidv ( 𝑧 = 𝑥 → ( ∀ 𝑦𝐴 ( 𝜓𝑧 = 𝑦 ) ↔ ∀ 𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )
12 11 cbvrexvw ( ∃ 𝑧𝐴𝑦𝐴 ( 𝜓𝑧 = 𝑦 ) ↔ ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) )
13 8 12 bitri ( ∃ 𝑧𝐴𝑥𝐴 ( 𝜑𝑥 = 𝑧 ) ↔ ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) )
14 13 anbi2i ( ( ∃ 𝑥𝐴 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( 𝜑𝑥 = 𝑧 ) ) ↔ ( ∃ 𝑥𝐴 𝜑 ∧ ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )
15 2 14 bitri ( ∃! 𝑥𝐴 𝜑 ↔ ( ∃ 𝑥𝐴 𝜑 ∧ ∃ 𝑥𝐴𝑦𝐴 ( 𝜓𝑥 = 𝑦 ) ) )