Definition df-reu 3347

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 3048). (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 3344	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2563	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3348  reubiia  3353  reubidva  3360  reueubd  3363  rmo5  3364  cbvreuvw  3368  reubida  3370  nfreu1  3374  nfreuw  3376  reueq1OLD  3380  reueqbidv  3384  cbvreu  3387  nfreud  3392  reuv  3465  reurab  3660  reu2  3684  reu6  3685  reu3  3686  2reuswap  3705  2reuswap2  3706  2reu5lem1  3714  cbvreucsf  3894  reuun2  4275  reuss2  4276  reupick  4279  reupick3  4280  euelss  4282  reusn  4680  rabsneu  4682  reusv2lem4  5339  reusv2lem5  5340  reuhypd  5357  funcnv3  6551  feu  6699  dff4  7034  f1ompt  7044  fsn  7068  riotauni  7309  riotacl2  7319  riota1  7324  riota1a  7325  riota2df  7326  snriota  7336  riotaund  7342  aceq1  10005  dfac2b  10019  nqerf  10818  zmin  12839  climreu  15460  divalglem10  16310  divalgb  16312  uptx  23538  txcn  23539  q1peqb  26086  axcontlem2  28941  edgnbusgreu  29343  nbusgredgeu0  29344  frgr3vlem2  30249  3vfriswmgrlem  30252  frgrncvvdeqlem2  30275  adjeu  31864  reuxfrdf  32465  rmoxfrd  32467  reueqi  36222  reueqbii  36223  cbvreuvw2  36262  cbvreudavw  36286  cbvreudavw2  36317  neibastop3  36395  cbvreud  37406  poimirlem25  37684  poimirlem27  37686  fsuppind  42622  onsucf1olem  43302  pairreueq  47540  prprsprreu  47549  prprreueq  47550  reutru  48834