Theorem reu7 3671

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

Hypothesis

Ref	Expression
rmo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
reu7	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu7

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reu3 3666	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧)))
2		rmo4.1	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2032	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4		equcom 2025	. . . . . . . 8 ⊢ (𝑦 = 𝑧 ↔ 𝑧 = 𝑦)
5	3, 4	syl6bb 290	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑧 = 𝑦))
6	2, 5	imbi12d 348	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑧 = 𝑦)))
7	6	cbvralvw 3396	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦))
8	7	rexbii 3210	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦))
9		equequ1 2032	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 ↔ 𝑥 = 𝑦))
10	9	imbi2d 344	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝜓 → 𝑧 = 𝑦) ↔ (𝜓 → 𝑥 = 𝑦)))
11	10	ralbidv 3162	. . . . 5 ⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
12	11	cbvrexvw 3397	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))
13	8, 12	bitri 278	. . 3 ⊢ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))
14	13	anbi2i 625	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
15	1, 14	bitri 278	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-10 2142  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clel 2870  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114

This theorem is referenced by:  cshwrepswhash1  16428