reu5 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > reu5		GIF version

Theorem reu5 2824

Description: Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)

**Assertion**
Ref	Expression
reu5	⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃*x ∈ A φ))

**Proof of Theorem reu5**
Step	Hyp	Ref	Expression
1		eu5 2242	. 2 ⊢ (∃!x(x ∈ A ∧ φ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃*x(x ∈ A ∧ φ)))
2		df-reu 2621	. 2 ⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
3		df-rex 2620	. . 3 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
4		df-rmo 2622	. . 3 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
5	3, 4	anbi12i 678	. 2 ⊢ ((∃x ∈ A φ ∧ ∃x ∈ A φ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃x(x ∈ A ∧ φ)))
6	1, 2, 5	3bitr4i 268	1 ⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃*x ∈ A φ))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 176 ∧ wa 358 ∃wex 1541 ∈ wcel 1710 ∃!weu 2204 ∃*wmo 2205 ∃wrex 2615 ∃!wreu 2616 ∃*wrmo 2617

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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

This theorem 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-rex 2620 df-reu 2621 df-rmo 2622

This theorem is referenced by: reurex 2825 reurmo 2826 reu4 3030 reueq 3033 fncnv 5158