Definition df-reu 3145

Description: Define restricted existential uniqueness.

Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-reu	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wreu 3140	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2653	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3328  nfreu1  3370  nfreud  3372  nfreuw  3374  reubida  3387  reubidva  3388  reubiia  3390  reueq1f  3399  reueq1  3407  reu5  3430  rmo5  3434  reueubd  3436  cbvreuw  3443  cbvreu  3447  reuv  3521  reu2  3716  reu6  3717  reu3  3718  2reuswap  3737  2reuswap2  3738  2reu5lem1  3746  cbvreucsf  3927  reuss2  4283  reuun2  4286  reupick  4287  reupick3  4288  euelss  4290  reusn  4663  rabsneu  4665  reusv2lem4  5302  reusv2lem5  5303  reuhypd  5320  funcnv3  6424  feu  6554  dff4  6867  f1ompt  6875  fsn  6897  riotauni  7120  riotacl2  7130  riota1  7135  riota1a  7136  riota2df  7137  snriota  7147  riotaund  7153  aceq1  9543  dfac2b  9556  nqerf  10352  zmin  12345  climreu  14913  divalglem10  15753  divalgb  15755  uptx  22233  txcn  22234  q1peqb  24748  axcontlem2  26751  edgnbusgreu  27149  nbusgredgeu0  27150  frgr3vlem2  28053  3vfriswmgrlem  28056  frgrncvvdeqlem2  28079  adjeu  29666  reuxfrdf  30255  rmoxfrd  30257  neibastop3  33710  cbvreud  34657  poimirlem25  34932  poimirlem27  34934  pairreueq  43721  prprsprreu  43730  prprreueq  43731