Definition df-reu 3368

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 3078). (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 3365	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2594	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3369  reubiia  3374  reubidva  3381  reueubd  3384  rmo5  3385  cbvreuvw  3389  reubida  3391  nfreu1  3395  nfreuw  3397  reueqbidv  3403  cbvreu  3406  nfreud  3411  reuv  3481  reurab  3663  reu2  3687  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  2reu5lem1  3717  cbvreucsf  3896  reuun2  4277  reuss2  4278  reupick  4281  reupick3  4282  euelss  4284  reusn  4692  rabsneu  4694  reusv2lem4  5372  reusv2lem5  5373  reuhypd  5390  funcnv3  6606  feu  6754  dff4  7096  f1ompt  7106  fsn  7131  riotauni  7373  riotacl2  7383  riota1  7388  riota1a  7389  riota2df  7390  snriota  7400  riotaund  7406  aceq1  10100  dfac2b  10113  nqerf  10914  zmin  12967  climreu  15606  divalglem10  16459  divalgb  16461  uptx  23761  txcn  23762  q1peqb  26292  axcontlem2  29281  edgnbusgreu  29683  nbusgredgeu0  29684  frgr3vlem2  30591  3vfriswmgrlem  30594  frgrncvvdeqlem2  30617  adjeu  32207  reuxfrdf  32803  rmoxfrd  32805  reueqi  36645  reueqbii  36646  cbvreuvw2  36685  cbvreudavw  36709  cbvreudavw2  36740  neibastop3  36817  cbvreud  37963  poimirlem25  38240  poimirlem27  38242  dfsuccl4  39069  fsuppind  43270  onsucf1olem  43945  pairreueq  48204  prprsprreu  48213  prprreueq  48214  reutru  49527