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

Definition df-rex 2361
Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
df-rex (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrex 2356 . 2 wff 𝑥𝐴 𝜑
52cv 1286 . . . . 5 class 𝑥
65, 3wcel 1436 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1424 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 103 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2365  rexnalim  2366  dfrex2dc  2367  rexbida  2371  rexbidv2  2379  rexbii2  2385  r2exf  2392  risset  2402  nfrexdxy  2407  nfrexdya  2409  nfre1  2415  rexex  2418  rspe  2420  rsp2e  2422  rexim  2463  reximi2  2465  reximdv2  2468  r19.23t  2475  r19.41  2518  r19.43  2521  reean  2531  rexeqf  2555  reu5  2575  rmo5  2578  cbvrexf  2581  cbvrexdva2  2591  rexv  2631  2gencl  2646  3gencl  2647  rspce  2710  rspcimedv  2717  ceqsrexv  2738  rexab  2768  rexab2  2772  rexrab2  2773  morex  2790  reu2  2794  reu6  2795  reu3  2796  2reuswapdc  2808  2rmorex  2810  cbvrexcsf  2980  rexun  3169  reuss2  3268  reuun2  3271  reupick  3272  reupick3  3273  reximdva0m  3287  rabn0r  3298  rabn0m  3299  r19.2m  3356  r19.9rmv  3360  rexm  3368  rexsns  3465  exsnrex  3468  dfuni2  3638  eluni2  3640  elunirab  3649  iuncom4  3720  iunxiun  3792  intexrabim  3964  bnd2  3983  rexxfrd  4259  elxp2  4429  opeliunxp  4461  xpiundi  4464  xpiundir  4465  rexiunxp  4546  dmuni  4614  rnmpt  4651  elrnmpt1  4654  elres  4715  dfima2  4743  dfima3  4744  elima2  4747  dfco2a  4897  imaco  4902  imadiflem  5058  imadif  5059  imainlem  5060  imain  5061  funimaexglem  5062  fvelrnb  5315  rexrnmpt  5405  dffo4  5410  dffo5  5411  abrexco  5499  opabex3d  5849  opabex3  5850  abexssex  5853  abexex  5854  ecexr  6249  mapsn  6399  mapsnen  6480  fimax2gtri  6569  ltexnqq  6911  subhalfnqq  6917  ltbtwnnq  6919  nqnq0  6944  prnmaxl  6991  prnminu  6992  prarloc  7006  genpdflem  7010  genpassl  7027  genpassu  7028  nqprm  7045  nqprl  7054  nqpru  7055  ltsopr  7099  ltexprlemm  7103  ltexprlemloc  7110  axprecex  7359  axpre-ltirr  7361  2rexuz  9002  ioom  9600  bdcuni  11212  bj-axun2  11251
  Copyright terms: Public domain W3C validator