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

Definition df-reu 2287
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 2282 . 2 wff ∃!x A φ
52cv 1225 . . . . 5 class x
65, 3wcel 1370 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2weu 1878 . 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  2455  nfreudxy  2457  reubida  2465  reubiia  2468  reueq1f  2477  reu5  2496  rmo5  2499  cbvreu  2505  reuv  2546  reu2  2702  reu6  2703  reu3  2704  2reuswapdc  2716  cbvreucsf  2883  reuss2  3190  reuun2  3193  reupick  3194  reupick3  3195  reusn  3411  rabsneu  3413  reuhypd  4149  funcnv3  4883  feu  4993  dff4im  5234  f1ompt  5241  fsn  5256  riotauni  5394  riotacl2  5401  riota1  5406  riota1a  5407  riota2df  5408  snriota  5417  riotaund  5422  acexmid  5431  bdcriota  7249
  Copyright terms: Public domain W3C validator