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

Definition df-reu 2475
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 2470 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1363 . . . . 5 class 𝑥
65, 3wcel 2160 . . . 4 wff 𝑥𝐴
76, 1wa 104 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2038 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 105 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2662  nfreudxy  2664  reubida  2672  reubiia  2675  reueq1f  2684  reu5  2703  rmo5  2706  cbvreu  2716  cbvreuvw  2724  reuv  2771  reu2  2940  reu6  2941  reu3  2942  2reuswapdc  2956  cbvreucsf  3136  reuss2  3430  reuun2  3433  reupick  3434  reupick3  3435  reusn  3678  rabsneu  3680  reuhypd  4489  funcnv3  5297  feu  5417  dff4im  5683  f1ompt  5688  fsn  5709  riotauni  5859  riotacl2  5866  riota1  5871  riota1a  5872  riota2df  5873  snriota  5882  riotaund  5887  acexmid  5896  climreu  11340  divalgb  11965  uptx  14251  txcn  14252  dedekindicc  14588  bdcriota  15113
  Copyright terms: Public domain W3C validator