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

Definition df-reu 2307
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu (∃!x A φ∃!x(x A φ))

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3wreu 2302 . 2 wff ∃!x A φ
52cv 1241 . . . . 5 class x
65, 3wcel 1390 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2weu 1897 . 2 wff ∃!x(x A φ)
94, 8wb 98 1 wff (∃!x A φ∃!x(x A φ))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2475  nfreudxy  2477  reubida  2485  reubiia  2488  reueq1f  2497  reu5  2516  rmo5  2519  cbvreu  2525  reuv  2567  reu2  2723  reu6  2724  reu3  2725  2reuswapdc  2737  cbvreucsf  2904  reuss2  3211  reuun2  3214  reupick  3215  reupick3  3216  reusn  3432  rabsneu  3434  reuhypd  4169  funcnv3  4904  feu  5015  dff4im  5256  f1ompt  5263  fsn  5278  riotauni  5417  riotacl2  5424  riota1  5429  riota1a  5430  riota2df  5431  snriota  5440  riotaund  5445  acexmid  5454  bdcriota  9338
  Copyright terms: Public domain W3C validator