MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ral Structured version   Visualization version   GIF version

Definition df-ral 3143
Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22.

Note: This notation is most often used to express that 𝜑 holds for all elements of a given class 𝐴. For this reading 𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather focus on those 𝑥 that happen to be contained in the corresponding 𝐴(𝑥). This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 43185 or ralndv2 43186, courtesy of AV.

So be careful to either keep 𝐴 independent of 𝑥, or adjust your comments to include such exotic cases. (Contributed by NM, 19-Aug-1993.)

Assertion
Ref Expression
df-ral (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wral 3138 . 2 wff 𝑥𝐴 𝜑
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1526 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 207 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  3148  alral  3154  raln  3155  ral2imi  3156  ralimi2  3157  ralbii2  3163  ralanidOLD  3169  r19.26m  3173  r19.21v  3175  ralimdv2  3176  hbralrimi  3180  ralbidv2  3195  r2allem  3200  r3al  3202  rsp  3205  r19.21t  3214  ralrimd  3218  nfra1  3219  hbral  3221  nfraldw  3223  nfrald  3224  rgen2a  3229  ralbida  3230  ralcom4  3235  r19.23t  3313  ralrexbid  3322  ralcom2w  3363  ralcom2  3364  rabid2  3382  rabid2f  3383  rabbi  3384  raleqf  3398  cbvralfw  3438  cbvralf  3440  cbvralvw  3450  cbvraldva2  3457  ralv  3520  ceqsralt  3529  rspct  3608  rspc  3610  rspcimdv  3612  rspc2gv  3631  ralxpxfr2d  3638  ralab  3683  ralab2  3687  ralab2OLD  3688  ralrab2  3689  reu2  3715  reu6  3716  reu3  3717  rmo4  3720  reu8  3723  rmo3f  3724  rmoim  3730  2reuswap  3736  2reuswap2  3737  2reu5lem2  3746  2reu5lem3  3747  2rmoswap  3751  rmo2  3869  rmo3  3871  rmo3OLD  3872  rmoanim  3877  cbvralcsf  3924  dfss3  3955  dfss3f  3958  ssabral  4041  ss2rab  4046  rabss  4047  ssrab  4048  dfdif3  4090  rexdifi  4121  ralunb  4166  reuss2  4282  n0el  4320  disj  4397  disj1  4399  r19.2z  4438  r19.3rz  4440  ralidm  4453  ralf0  4455  falseral0  4457  rabsssn  4599  ralsnsg  4600  unissb  4863  dfint2  4871  elint2  4876  elintrab  4881  ssintrab  4892  dfiin2g  4949  invdisj  5042  disjss3  5057  dftr5  5167  reusv2lem4  5293  axprlem2  5316  axprlem4  5318  axprlem5  5319  raliunxp  5704  dmopab3  5782  asymref  5970  asymref2  5971  dffun7  6376  funcnv  6417  fnres  6468  mptfnf  6477  fnopabg  6479  dff3  6859  dffo3  6861  find  7595  funcnvuni  7624  zfrep6  7647  nfixpw  8469  nfixp  8470  marypha2lem3  8890  zfregcl  9047  zfinf2  9094  scottexs  9305  scott0s  9306  aceq1  9532  aceq2  9534  kmlem12  9576  kmlem14  9578  kmlem15  9579  zorn2lem4  9910  zorn2lem5  9911  ingru  10226  axgroth5  10235  grothprim  10245  sstskm  10253  supsrlem  10522  infm3  11589  nnunb  11882  nnwos  12304  fz1sbc  12973  cotr2g  14326  caubnd  14708  rpnnen2lem12  15568  isprm2  16016  pgpfac1  19133  pgpfac  19137  lidldvgen  19958  iunocv  20755  istopg  21433  dfconn2  21957  1stccn  22001  iskgen3  22087  fbfinnfr  22379  iscmet3  23825  wilthlem3  25575  isch3  28946  choc0  29031  pjnormssi  29873  nelbOLD  30160  moel  30180  reuxfrdf  30183  inpr0  30220  ssiun3  30239  fmcncfil  31074  bnj115  31895  bnj946  31946  bnj1142  31961  bnj1211  31969  bnj1294  31989  bnj1385  32004  bnj110  32030  bnj611  32090  bnj864  32094  bnj865  32095  bnj1000  32113  bnj978  32121  bnj1049  32144  bnj1090  32149  bnj1133  32159  bnj1176  32175  bnj1186  32177  bnj1253  32187  bnj1388  32203  untuni  32833  dfpo2  32889  dfon2lem8  32933  wzel  33009  dfrdg4  33310  onsuct0  33687  bj-ralvw  34093  bj-rcleqf  34235  exrecfnlem  34543  fvineqsneq  34576  poimirlem25  34799  poimirlem30  34804  nninfnub  34909  mptbi12f  35327  pmapglbx  36787  cdlemefrs29bpre0  37414  sn-axrep5v  38988  dford4  39506  cllem0  39805  elmapintrab  39816  elintima  39878  ss2iundf  39884  ntrneiiso  40321  ntrneik2  40322  ntrneix2  40323  ntrneikb  40324  scottabf  40456  expandral  40506  ralbidar  40657  rexbidar  40658  ssralv2  40745  en3lpVD  41059  ssralv2VD  41080  trintALTVD  41094  ssrabf  41262  rabssf  41266  dffo3f  41318  rexrsb  43179  nrhmzr  44042  empty-surprise  44781  alsconv  44789
  Copyright terms: Public domain W3C validator