Definition df-reu 3366

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

This definition is used by:  reu5  3367  reubiia  3372  reubidva  3379  reueubd  3382  rmo5  3383  cbvreuvw  3387  reubida  3389  nfreu1  3393  nfreuw  3395  reueqbidv  3401  cbvreu  3404  nfreud  3409  reuv  3478  reurab  3658  reu2  3682  reu6  3683  reu3  3684  2reuswap  3703  2reuswap2  3704  2reu5lem1  3712  cbvreucsf  3890  reuun2  4270  reuss2  4271  reupick  4274  reupick3  4275  euelss  4277  reusn  4687  rabsneu  4689  reusv2lem4  5362  reusv2lem5  5363  reuhypd  5380  funcnv3  6598  feu  6746  dff4  7089  f1ompt  7099  fsn  7124  riotauni  7371  riotacl2  7381  riota1  7386  riota1a  7387  riota2df  7388  snriota  7398  riotaund  7404  aceq1  10167  dfac2b  10180  nqerf  10986  zmin  13040  climreu  15690  divalglem10  16539  divalgb  16541  uptx  23905  txcn  23906  q1peqb  26435  axcontlem2  29476  edgnbusgreu  29881  nbusgredgeu0  29882  frgr3vlem2  30808  3vfriswmgrlem  30811  frgrncvvdeqlem2  30834  adjeu  32424  reuxfrdf  33020  rmoxfrd  33022  reueqi  36900  reueqbii  36901  cbvreuvw2  36940  cbvreudavw  36964  cbvreudavw2  36995  neibastop3  37072  cbvreud  38216  poimirlem25  38483  poimirlem27  38485  dfsuccl4  39326  fsuppind  43540  onsucf1olem  44215  pairreueq  48514  prprsprreu  48523  prprreueq  48524  reutru  49836  dfralseu2  50841