Definition df-reu 3370

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 3081). (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 3367	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2596	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3371  reubiia  3376  reubidva  3383  reueubd  3386  rmo5  3387  cbvreuvw  3391  reubida  3393  nfreu1  3397  nfreuw  3399  reueqbidv  3405  cbvreu  3408  nfreud  3413  reuv  3482  reurab  3662  reu2  3686  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  2reu5lem1  3716  cbvreucsf  3895  reuun2  4273  reuss2  4274  reupick  4277  reupick3  4278  euelss  4280  reusn  4688  rabsneu  4690  reusv2lem4  5367  reusv2lem5  5368  reuhypd  5385  funcnv3  6629  feu  6777  dff4  7122  f1ompt  7132  fsn  7157  riotauni  7403  riotacl2  7413  riota1  7418  riota1a  7419  riota2df  7420  snriota  7430  riotaund  7436  aceq1  10220  dfac2b  10233  nqerf  11039  zmin  13095  climreu  15749  divalglem10  16598  divalgb  16600  uptx  23971  txcn  23972  q1peqb  26501  axcontlem2  29570  edgnbusgreu  29975  nbusgredgeu0  29976  frgr3vlem2  30902  3vfriswmgrlem  30905  frgrncvvdeqlem2  30928  adjeu  32518  reuxfrdf  33156  rmoxfrd  33158  reu6f  35776  reueqi  37155  reueqbii  37156  cbvreuvw2  37195  cbvreudavw  37219  cbvreudavw2  37250  neibastop3  37327  cbvreud  38487  poimirlem25  38754  poimirlem27  38756  dfsuccl4  39597  fsuppind  43809  onsucf1olem  44462  pairreueq  48795  prprsprreu  48804  prprreueq  48805  reutru  50117  dfralseu2  51197