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 3047
Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (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 3042 . 2 wff 𝑥𝐴 𝜑
52cv 1623 . . . . 5 class 𝑥
65, 3wcel 2131 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1622 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  3052  alral  3058  rsp  3059  r2allem  3067  r3al  3070  nfra1  3071  hbral  3073  nfrald  3074  ral2imi  3077  ralimi2  3079  hbralrimi  3084  r19.21t  3085  ralrimd  3089  r19.21v  3090  ralimdv2  3091  rgen2a  3107  ralbii2  3108  ralbida  3112  ralbidv2  3114  raln  3121  ralnexOLD  3123  r19.23t  3151  r19.26m  3197  ralcom2  3234  rabid2  3249  rabid2f  3250  rabbi  3251  raleqf  3265  cbvralf  3296  cbvraldva2  3306  ralv  3351  ceqsralt  3361  rspct  3434  rspc  3435  rspcimdv  3442  rspc2gv  3452  ralxpxfr2d  3458  ralab  3500  ralab2  3504  ralrab2  3505  reu2  3527  reu6  3528  reu3  3529  rmo4  3532  reu8  3535  rmoim  3540  2reuswap  3543  2reu5lem2  3547  2reu5lem3  3548  rmo2  3659  rmo3  3661  cbvralcsf  3698  dfss3  3725  dfss3f  3728  ssabral  3806  ss2rab  3811  rabss  3812  ssrab  3813  dfdif3  3855  ralunb  3929  reuss2  4042  n0el  4075  disj  4152  disj1  4154  r19.2z  4196  r19.3rz  4198  ralidm  4211  ralf0  4214  ralf0OLD  4215  falseral0  4217  rabsssn  4351  ralsnsg  4352  unissb  4613  dfint2  4621  elint2  4626  elintrab  4632  ssintrab  4644  dfiin2g  4697  invdisj  4782  disjss3  4795  dftr5  4899  trint  4912  reusv2lem4  5013  raliunxp  5409  dmopab3  5484  issref  5659  asymref  5662  asymref2  5663  dffun7  6068  funcnv  6111  fnres  6160  mptfnf  6168  fnopabg  6170  dff3  6527  dffo3  6529  find  7248  funcnvuni  7276  zfrep6  7291  nfixp  8085  marypha2lem3  8500  zfregcl  8656  zfinf2  8704  scottexs  8915  scott0s  8916  aceq1  9122  aceq2  9124  kmlem12  9167  kmlem14  9169  kmlem15  9170  zorn2lem4  9505  zorn2lem5  9506  ingru  9821  axgroth5  9830  grothprim  9840  sstskm  9848  supsrlem  10116  infm3  11166  nnunb  11472  nnwos  11940  fz1sbc  12601  cotr2g  13908  caubnd  14289  rpnnen2lem12  15145  isprm2  15589  pgpfac1  18671  pgpfac  18675  lidldvgen  19449  iunocv  20219  istopg  20894  dfconn2  21416  1stccn  21460  iskgen3  21546  fbfinnfr  21838  iscmet3  23283  wilthlem3  24987  isch3  28399  choc0  28486  pjnormssi  29328  moel  29624  2reuswap2  29628  rmo3f  29635  rmo4fOLD  29636  ssiun3  29675  fmcncfil  30278  bnj115  31092  bnj538OLD  31109  bnj946  31144  bnj1142  31159  bnj1211  31167  bnj1294  31187  bnj1385  31202  bnj110  31227  bnj611  31287  bnj864  31291  bnj865  31292  bnj1000  31310  bnj978  31318  bnj1049  31341  bnj1090  31346  bnj1133  31356  bnj1176  31372  bnj1186  31374  bnj1253  31384  bnj1388  31400  untuni  31885  dfpo2  31944  dfon2lem8  31992  wzel  32067  dfrdg4  32356  onsuct0  32738  bj-ralvw  33163  bj-ralcom4  33166  bj-raldifsn  33352  bj-ismooredr  33362  poimirlem25  33739  poimirlem30  33744  nninfnub  33852  mptbi12f  34280  ralanid  34327  pmapglbx  35550  cdlemefrs29bpre0  36178  dford4  38090  cllem0  38365  elmapintrab  38376  elintima  38439  ss2iundf  38445  ntrneiiso  38883  ntrneik2  38884  ntrneix2  38885  ntrneikb  38886  ralbidar  39143  rexbidar  39144  ssralv2  39231  en3lpVD  39571  ssralv2VD  39593  trintALTVD  39607  ssrabf  39789  rabssf  39793  dffo3f  39855  rexrsb  41667  2rmoswap  41682  nrhmzr  42375  empty-surprise  43033  alsconv  43041
  Copyright terms: Public domain W3C validator