Theorem reu7 3032

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

Hypothesis

Ref	Expression
rmo4.1	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
reu7	⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃x ∈ A ∀y ∈ A (ψ → x = y)))

Distinct variable groups:   x,y,A   φ,y   ψ,x

Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem reu7

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reu3 3027	. 2 ⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃z ∈ A ∀x ∈ A (φ → x = z)))
2		rmo4.1	. . . . . . 7 ⊢ (x = y → (φ ↔ ψ))
3		eqeq1 2359	. . . . . . . 8 ⊢ (x = y → (x = z ↔ y = z))
4		eqcom 2355	. . . . . . . 8 ⊢ (y = z ↔ z = y)
5	3, 4	syl6bb 252	. . . . . . 7 ⊢ (x = y → (x = z ↔ z = y))
6	2, 5	imbi12d 311	. . . . . 6 ⊢ (x = y → ((φ → x = z) ↔ (ψ → z = y)))
7	6	cbvralv 2836	. . . . 5 ⊢ (∀x ∈ A (φ → x = z) ↔ ∀y ∈ A (ψ → z = y))
8	7	rexbii 2640	. . . 4 ⊢ (∃z ∈ A ∀x ∈ A (φ → x = z) ↔ ∃z ∈ A ∀y ∈ A (ψ → z = y))
9		eqeq1 2359	. . . . . . 7 ⊢ (z = x → (z = y ↔ x = y))
10	9	imbi2d 307	. . . . . 6 ⊢ (z = x → ((ψ → z = y) ↔ (ψ → x = y)))
11	10	ralbidv 2635	. . . . 5 ⊢ (z = x → (∀y ∈ A (ψ → z = y) ↔ ∀y ∈ A (ψ → x = y)))
12	11	cbvrexv 2837	. . . 4 ⊢ (∃z ∈ A ∀y ∈ A (ψ → z = y) ↔ ∃x ∈ A ∀y ∈ A (ψ → x = y))
13	8, 12	bitri 240	. . 3 ⊢ (∃z ∈ A ∀x ∈ A (φ → x = z) ↔ ∃x ∈ A ∀y ∈ A (ψ → x = y))
14	13	anbi2i 675	. 2 ⊢ ((∃x ∈ A φ ∧ ∃z ∈ A ∀x ∈ A (φ → x = z)) ↔ (∃x ∈ A φ ∧ ∃x ∈ A ∀y ∈ A (ψ → x = y)))
15	1, 14	bitri 240	1 ⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃x ∈ A ∀y ∈ A (ψ → x = y)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642  ∀wral 2615  ∃wrex 2616  ∃!wreu 2617

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is used by: (None)