ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-reu GIF version

Definition df-reu 2313
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wreu 2308 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1242 . . . . 5 class 𝑥
65, 3wcel 1393 . . . 4 wff 𝑥𝐴
76, 1wa 97 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 1900 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 98 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2481  nfreudxy  2483  reubida  2491  reubiia  2494  reueq1f  2503  reu5  2522  rmo5  2525  cbvreu  2531  reuv  2573  reu2  2729  reu6  2730  reu3  2731  2reuswapdc  2743  cbvreucsf  2910  reuss2  3217  reuun2  3220  reupick  3221  reupick3  3222  reusn  3441  rabsneu  3443  reuhypd  4203  funcnv3  4961  feu  5072  dff4im  5313  f1ompt  5320  fsn  5335  riotauni  5474  riotacl2  5481  riota1  5486  riota1a  5487  riota2df  5488  snriota  5497  riotaund  5502  acexmid  5511  climreu  9818  bdcriota  10003
  Copyright terms: Public domain W3C validator