Definition df-ral 3051

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 47059 or ralndv2 47060, 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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wral 3050	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1537	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3052  raln  3058  alral  3064  ralimi2  3067  ral2imi  3074  ralbii2  3077  ralrexbidOLD  3094  r19.26m  3097  r2allem  3129  hbralrimi  3131  ralimdv2  3150  ralbidv2  3161  r19.21vOLD  3168  r3al  3184  rspw  3223  cbvralvw  3224  rsp  3234  r19.21t  3240  r19.23t  3242  ralrimd  3251  nfra1  3270  ralcom4  3272  cbvralfw  3288  hbral  3292  nfraldw  3293  cbvralsvw  3301  raleqbidvvOLD  3319  cbvraldva2  3332  raleqf  3337  sbralie  3342  cbvralf  3344  rgen2a  3355  nfrald  3356  ralcom2  3361  moelOLD  3389  rabbi  3451  rabid2f  3452  rabid2im  3453  rabid2OLD  3455  ralv  3492  ceqsralt  3500  rspct  3592  rspc  3594  rspcimdv  3596  rspc2gv  3616  ralxpxfr2d  3630  ralab  3681  ralabOLD  3682  ralab2  3687  ralrab2  3688  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  rmoanim  3876  cbvralcsf  3923  dfss3  3954  dfss3f  3957  ssralv  4034  ralss  4040  ssabral  4047  ss2rab  4053  rabss  4054  ssrab  4055  dfdif3OLD  4100  rexdifi  4132  ralunb  4179  reuss2  4308  rspn0  4338  n0el  4346  disj  4432  disj1  4434  r19.2z  4477  r19.3rz  4479  ralidmw  4490  rzal  4491  ralidm  4494  ralf0  4496  falseral0  4498  rabsssn  4650  ralsnsg  4652  ralsng  4657  unissb  4921  unissbOLD  4922  dfint2  4930  elint2  4935  elintrab  4942  ssintrab  4953  dfiin2g  5014  invdisj  5111  disjss3  5124  dftr5  5245  dftr5OLD  5246  reusv2lem4  5383  axprlem2  5406  axprlem4  5408  axprlem4OLD  5411  axprlem5OLD  5412  dffr6  5622  raliunxp  5832  dmopab3  5912  rnopab3  5949  asymref  6118  asymref2  6119  dfpo2  6298  dffun7  6574  funcnv  6616  fnres  6676  mptfnf  6684  fnopabg  6686  dff3  7101  dffo3  7103  dffo3f  7107  fnssintima  7365  imaeqalov  7655  find  7900  funcnvuni  7937  zfrep6  7962  ralxp3f  8145  frpoins3xpg  8148  frpoins3xp3g  8149  nfixpw  8939  nfixp  8940  marypha2lem3  9460  zfregcl  9617  zfinf2  9665  scottexs  9910  scott0s  9911  aceq1  10140  aceq2  10142  kmlem12  10185  kmlem14  10187  kmlem15  10188  zorn2lem4  10522  zorn2lem5  10523  ingru  10838  axgroth5  10847  grothprim  10857  sstskm  10865  supsrlem  11134  infm3  12210  nnunb  12506  nnwos  12940  fz1sbc  13623  cotr2g  14998  caubnd  15380  rpnnen2lem12  16244  isprm2  16702  pgpfac1  20069  pgpfac  20073  nrhmzr  20506  lidldvgen  21307  iunocv  21662  ismhp3  22109  istopg  22864  dfconn2  23388  1stccn  23432  iskgen3  23518  fbfinnfr  23810  iscmet3  25278  wilthlem3  27064  eqscut2  27802  elons2  28232  isch3  31203  choc0  31288  pjnormssi  32130  reuxfrdf  32453  rabsspr  32463  rabsstp  32464  inpr0  32493  ssiun3  32514  ssdifidlprm  33423  fmcncfil  33867  bnj115  34676  bnj946  34725  bnj1142  34740  bnj1211  34748  bnj1294  34768  bnj1385  34783  bnj110  34809  bnj611  34869  bnj864  34873  bnj865  34874  bnj1000  34892  bnj978  34900  bnj1049  34925  bnj1090  34930  bnj1133  34940  bnj1176  34956  bnj1186  34958  bnj1253  34968  bnj1388  34984  untuni  35646  dfon2lem8  35728  wzel  35762  dfrdg4  35889  ixpeq12dv  36154  cbvralvw2  36164  onsuct0  36379  bj-ralvw  36817  bj-rcleqf  36963  exrecfnlem  37317  fvineqsneq  37350  poimirlem25  37589  poimirlem30  37594  nninfnub  37695  mptbi12f  38110  pmapglbx  39708  cdlemefrs29bpre0  40335  sn-axrep5v  42192  dford4  42982  unielss  43171  orddif0suc  43222  cllem0  43520  elmapintrab  43530  elintima  43607  ss2iundf  43613  ntrneiiso  44045  ntrneik2  44046  ntrneix2  44047  ntrneikb  44048  scottabf  44200  expandral  44250  ismnushort  44261  ralbidar  44405  rexbidar  44406  ssralv2  44492  en3lpVD  44806  ssralv2VD  44827  trintALTVD  44841  traxext  44935  dfac5prim  44948  ssrabf  45060  rabssf  45065  r19.3rzf  45104  rexrsb  47054  empty-surprise  49293  alsconv  49301