Definition df-reu 3381

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 3062). (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 3378	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2568	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3382  reubiia  3387  reuanidOLD  3393  reubidva  3396  reueubd  3399  rmo5  3400  cbvreuvw  3404  reubida  3407  nfreu1  3412  nfreuw  3414  cbvreuwOLD  3415  reueq1OLD  3419  reueqbidv  3423  nfreuwOLD  3426  cbvreu  3428  nfreud  3433  reuv  3510  reurab  3707  reu2  3731  reu6  3732  reu3  3733  2reuswap  3752  2reuswap2  3753  2reu5lem1  3761  cbvreucsf  3943  reuun2  4325  reuss2  4326  reupick  4329  reupick3  4330  euelss  4332  reusn  4727  rabsneu  4729  reusv2lem4  5401  reusv2lem5  5402  reuhypd  5419  funcnv3  6636  feu  6784  dff4  7121  f1ompt  7131  fsn  7155  riotauni  7394  riotacl2  7404  riota1  7409  riota1a  7410  riota2df  7411  snriota  7421  riotaund  7427  aceq1  10157  dfac2b  10171  nqerf  10970  zmin  12986  climreu  15592  divalglem10  16439  divalgb  16441  uptx  23633  txcn  23634  q1peqb  26195  axcontlem2  28980  edgnbusgreu  29384  nbusgredgeu0  29385  frgr3vlem2  30293  3vfriswmgrlem  30296  frgrncvvdeqlem2  30319  adjeu  31908  reuxfrdf  32510  rmoxfrd  32512  reueqi  36190  reueqbii  36191  cbvreuvw2  36230  cbvreudavw  36254  cbvreudavw2  36285  neibastop3  36363  cbvreud  37374  poimirlem25  37652  poimirlem27  37654  fsuppind  42600  onsucf1olem  43283  pairreueq  47497  prprsprreu  47506  prprreueq  47507  reutru  48724