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 2946
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 2941 . 2 wff 𝑥𝐴 𝜑
52cv 1522 . . . . 5 class 𝑥
65, 3wcel 2030 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1521 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  2951  alral  2957  rsp  2958  r2allem  2966  r3al  2969  nfra1  2970  hbral  2972  nfrald  2973  ral2imi  2976  ralimi2  2978  hbralrimi  2983  r19.21t  2984  ralrimd  2988  r19.21v  2989  ralimdv2  2990  rgen2a  3006  ralbii2  3007  ralbida  3011  ralbidv2  3013  raln  3020  ralnexOLD  3022  r19.23t  3050  r19.26m  3096  ralcom2  3133  rabid2  3148  rabid2f  3149  rabbi  3150  raleqf  3164  cbvralf  3195  cbvraldva2  3205  ralv  3250  ceqsralt  3260  rspct  3333  rspc  3334  rspcimdv  3341  rspc2gv  3352  ralxpxfr2d  3358  ralab  3400  ralab2  3404  ralrab2  3405  reu2  3427  reu6  3428  reu3  3429  rmo4  3432  reu8  3435  rmoim  3440  2reuswap  3443  2reu5lem2  3447  2reu5lem3  3448  rmo2  3559  rmo3  3561  cbvralcsf  3598  dfss3  3625  dfss3f  3628  ssabral  3706  ss2rab  3711  rabss  3712  ssrab  3713  ralunb  3827  reuss2  3940  n0el  3973  disj  4050  disj1  4052  r19.2z  4093  r19.3rz  4095  ralidm  4108  ralf0  4111  ralf0OLD  4112  falseral0  4114  rabsssn  4247  ralsnsg  4248  unissb  4501  dfint2  4509  elint2  4514  elintrab  4520  ssintrab  4532  dfiin2g  4585  invdisj  4670  disjss3  4684  dftr5  4788  trint  4801  reusv2lem4  4902  raliunxp  5294  dmopab3  5369  issref  5544  asymref  5547  asymref2  5548  dffun7  5953  funcnv  5996  fnres  6045  mptfnf  6053  fnopabg  6055  dff3  6412  dffo3  6414  find  7133  funcnvuni  7161  zfrep6  7176  nfixp  7969  marypha2lem3  8384  zfregcl  8540  zfinf2  8577  scottexs  8788  scott0s  8789  aceq1  8978  aceq2  8980  kmlem12  9021  kmlem14  9023  kmlem15  9024  zorn2lem4  9359  zorn2lem5  9360  ingru  9675  axgroth5  9684  grothprim  9694  sstskm  9702  supsrlem  9970  infm3  11020  nnunb  11326  nnwos  11793  fz1sbc  12454  cotr2g  13761  caubnd  14142  rpnnen2lem12  14998  isprm2  15442  pgpfac1  18525  pgpfac  18529  lidldvgen  19303  iunocv  20073  istopg  20748  dfconn2  21270  1stccn  21314  iskgen3  21400  fbfinnfr  21692  iscmet3  23137  wilthlem3  24841  isch3  28226  choc0  28313  pjnormssi  29155  moel  29451  2reuswap2  29455  rmo3f  29462  rmo4fOLD  29463  ssiun3  29502  fmcncfil  30105  bnj115  30919  bnj538OLD  30936  bnj946  30971  bnj1142  30986  bnj1211  30994  bnj1294  31014  bnj1385  31029  bnj110  31054  bnj611  31114  bnj864  31118  bnj865  31119  bnj1000  31137  bnj978  31145  bnj1049  31168  bnj1090  31173  bnj1133  31183  bnj1176  31199  bnj1186  31201  bnj1253  31211  bnj1388  31227  untuni  31712  dfpo2  31771  dfon2lem8  31819  wzel  31894  dfrdg4  32183  onsuct0  32565  bj-ralvw  32990  bj-ralcom4  32993  bj-raldifsn  33179  bj-ismooredr  33189  poimirlem25  33564  poimirlem30  33569  nninfnub  33677  mptbi12f  34105  ralanid  34152  pmapglbx  35373  cdlemefrs29bpre0  36001  dford4  37913  cllem0  38188  elmapintrab  38199  elintima  38262  ss2iundf  38268  ntrneiiso  38706  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  ralbidar  38966  rexbidar  38967  ssralv2  39054  en3lpVD  39394  ssralv2VD  39416  trintALTVD  39430  ssrabf  39612  rabssf  39616  dffo3f  39678  rexrsb  41490  2rmoswap  41505  nrhmzr  42198  empty-surprise  42856  alsconv  42864
  Copyright terms: Public domain W3C validator