Definition df-reu 3355

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

This definition is referenced by:  reu5  3356  reubiia  3361  reuanidOLD  3367  reubidva  3370  reueubd  3373  rmo5  3374  cbvreuvw  3378  reubida  3380  nfreu1  3384  nfreuw  3386  reueq1OLD  3390  reueqbidv  3394  cbvreu  3397  nfreud  3402  reuv  3476  reurab  3672  reu2  3696  reu6  3697  reu3  3698  2reuswap  3717  2reuswap2  3718  2reu5lem1  3726  cbvreucsf  3906  reuun2  4288  reuss2  4289  reupick  4292  reupick3  4293  euelss  4295  reusn  4691  rabsneu  4693  reusv2lem4  5356  reusv2lem5  5357  reuhypd  5374  funcnv3  6586  feu  6736  dff4  7073  f1ompt  7083  fsn  7107  riotauni  7350  riotacl2  7360  riota1  7365  riota1a  7366  riota2df  7367  snriota  7377  riotaund  7383  aceq1  10070  dfac2b  10084  nqerf  10883  zmin  12903  climreu  15522  divalglem10  16372  divalgb  16374  uptx  23512  txcn  23513  q1peqb  26061  axcontlem2  28892  edgnbusgreu  29294  nbusgredgeu0  29295  frgr3vlem2  30203  3vfriswmgrlem  30206  frgrncvvdeqlem2  30229  adjeu  31818  reuxfrdf  32420  rmoxfrd  32422  reueqi  36177  reueqbii  36178  cbvreuvw2  36217  cbvreudavw  36241  cbvreudavw2  36272  neibastop3  36350  cbvreud  37361  poimirlem25  37639  poimirlem27  37641  fsuppind  42578  onsucf1olem  43259  pairreueq  47511  prprsprreu  47520  prprreueq  47521  reutru  48792