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

Definition df-reu 2382
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 2377 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1298 . . . . 5 class 𝑥
65, 3wcel 1448 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 1960 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 104 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2560  nfreudxy  2562  reubida  2570  reubiia  2573  reueq1f  2582  reu5  2601  rmo5  2604  cbvreu  2610  reuv  2660  reu2  2825  reu6  2826  reu3  2827  2reuswapdc  2841  cbvreucsf  3014  reuss2  3303  reuun2  3306  reupick  3307  reupick3  3308  reusn  3541  rabsneu  3543  reuhypd  4330  funcnv3  5121  feu  5241  dff4im  5498  f1ompt  5503  fsn  5524  riotauni  5668  riotacl2  5675  riota1  5680  riota1a  5681  riota2df  5682  snriota  5691  riotaund  5696  acexmid  5705  climreu  10905  divalgb  11417  uptx  12224  txcn  12225  bdcriota  12662
  Copyright terms: Public domain W3C validator