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

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 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )