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