NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-rex GIF version

Definition df-rex 2620
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 (x A φx(x A φ))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3wrex 2615 . 2 wff x A φ
52cv 1641 . . . . 5 class x
65, 3wcel 1710 . . . 4 wff x A
76, 1wa 358 . . 3 wff (x A φ)
87, 2wex 1541 . 2 wff x(x A φ)
94, 8wb 176 1 wff (x A φx(x A φ))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2624  rexnal  2625  rexbida  2629  rexbidv2  2637  rexbii2  2643  r2exf  2650  risset  2661  nfre1  2670  rexex  2673  rspe  2675  rsp2e  2677  reximi2  2720  reximdv2  2723  r19.23t  2728  r19.41  2763  reean  2777  rexeqf  2804  reu5  2824  rmo5  2827  cbvrexdva2  2840  rexv  2873  2gencl  2888  3gencl  2889  rspce  2950  ceqsrexv  2972  rexab  2999  rexab2  3003  rexrab2  3004  morex  3020  reu2  3024  reu6  3025  reu3  3026  2reuswap  3038  2reu5lem3  3043  2reu5  3044  rexun  3443  reuss2  3535  reuun2  3538  reupick  3539  reupick3  3540  reximdva0  3561  rabn0  3570  r19.2z  3639  r19.2zb  3640  rexsns  3764  dfuni2  3893  eluni2  3895  elunirab  3904  iuncom4  3976  iunxiun  4048  elpw1  4144  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  opkelimagekg  4271  imacok  4282  dfimak2  4298  dfpw12  4301  ndisjrelk  4323  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  elsuc  4413  addcass  4415  nnsucelrlem1  4424  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  nnpw1ex  4484  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspss  4551  vfinncsp  4554  dfop2lem1  4573  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  elima2  4755  elima3  4756  elxp2  4802  xpiundi  4817  xpiundir  4818  opeliunxp  4820  dmuni  4914  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  dfima4  4952  rnopab2  4968  elres  4995  imadmrn  5008  rnuni  5038  dfco2a  5081  imaco  5086  dfcnv2  5100  iunfopab  5204  fnrnfv  5364  dffo4  5423  dffo5  5424  abrexco  5463  isomin  5496  dmsi  5519  disjex  5823  addcfnex  5824  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  frds  5935  mapsn  6026  xpassen  6057  enpw1pw  6075  mucex  6133  ncspw1eu  6159  el2c  6191  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  taddc  6229  tcfnex  6244
  Copyright terms: Public domain W3C validator