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

Definition df-reu 2282
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 2277 . 2 wff ∃!x A φ
52cv 1222 . . . . 5 class x
65, 3wcel 1366 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2weu 1873 . 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  2450  nfreudxy  2452  reubida  2460  reubiia  2463  reueq1f  2472  reu5  2491  rmo5  2494  cbvreu  2500  reuv  2541  reu2  2697  reu6  2698  reu3  2699  2reuswapdc  2711  cbvreucsf  2878  reuss2  3185  reuun2  3188  reupick  3189  reupick3  3190  reusn  3404  rabsneu  3406  reuhypd  4141  funcnv3  4875  feu  4985  dff4im  5226  f1ompt  5233  fsn  5248  riotauni  5386  riotacl2  5393  riota1  5398  riota1a  5399  riota2df  5400  snriota  5409  riotaund  5414  acexmid  5423  bdcriota  8268
  Copyright terms: Public domain W3C validator