Definition df-ral 3068

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 44484 or ralndv2 44485, 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 3063	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1537	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 205	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3073  alral  3079  raln  3080  ral2imi  3081  ralimi2  3083  ralbii2  3088  r19.26m  3097  r19.21v  3100  ralimdv2  3101  hbralrimi  3105  ralbidv2  3118  r2allem  3123  r3al  3125  rspw  3128  rsp  3129  r19.21t  3137  ralrimd  3141  nfra1  3142  hbral  3144  nfraldw  3146  nfraldwOLD  3147  nfrald  3148  nfra2wOLD  3152  rgen2a  3155  ralbidaOLD  3157  ralcom4  3161  ralcom4OLD  3162  r19.23t  3241  ralrexbidOLD  3251  ralcom2  3288  rabid2  3307  rabid2f  3308  rabbi  3309  raleqf  3323  raleqbidvv  3329  moel  3349  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  cbvralvw  3372  cbvraldva2  3381  ralv  3446  ceqsralt  3453  rspct  3537  rspc  3539  rspcimdv  3541  rspc2gv  3561  ralxpxfr2d  3568  ralab  3621  ralabOLD  3622  ralab2  3627  ralab2OLD  3628  ralrab2  3629  reu2  3655  reu6  3656  reu3  3657  rmo4  3660  reu8  3663  rmo3f  3664  rmoim  3670  2reuswap  3676  2reuswap2  3677  2reu5lem2  3686  2reu5lem3  3687  2rmoswap  3691  rmo2  3816  rmo3  3818  rmoanim  3823  cbvralcsf  3873  dfss3  3905  dfss3f  3908  ssabral  3992  ss2rab  4000  rabss  4001  ssrab  4002  dfdif3  4045  rexdifi  4076  ralunb  4121  reuss2  4246  rspn0  4283  n0el  4292  disj  4378  disjOLD  4379  disj1  4381  r19.2z  4422  r19.3rz  4424  ralidmw  4435  rzal  4436  ralidm  4439  ralf0  4441  ralidmOLD  4443  ralf0OLD  4445  falseral0  4447  rabsssn  4600  ralsnsg  4601  ralsng  4606  unissb  4870  dfint2  4878  elint2  4883  elintrab  4888  ssintrab  4899  dfiin2g  4958  invdisj  5054  disjss3  5069  dftr5  5190  reusv2lem4  5319  axprlem2  5342  axprlem4  5344  axprlem5  5345  dffr6  5538  raliunxp  5737  dmopab3  5817  asymref  6010  asymref2  6011  dfpo2  6188  dffun7  6445  funcnv  6487  fnres  6543  mptfnf  6552  fnopabg  6554  dff3  6958  dffo3  6960  find  7717  findOLD  7718  funcnvuni  7752  zfrep6  7771  nfixpw  8662  nfixp  8663  marypha2lem3  9126  zfregcl  9283  zfinf2  9330  scottexs  9576  scott0s  9577  aceq1  9804  aceq2  9806  kmlem12  9848  kmlem14  9850  kmlem15  9851  zorn2lem4  10186  zorn2lem5  10187  ingru  10502  axgroth5  10511  grothprim  10521  sstskm  10529  supsrlem  10798  infm3  11864  nnunb  12159  nnwos  12584  fz1sbc  13261  cotr2g  14615  caubnd  14998  rpnnen2lem12  15862  isprm2  16315  pgpfac1  19598  pgpfac  19602  lidldvgen  20439  iunocv  20798  ismhp3  21243  istopg  21952  dfconn2  22478  1stccn  22522  iskgen3  22608  fbfinnfr  22900  iscmet3  24362  wilthlem3  26124  isch3  29504  choc0  29589  pjnormssi  30431  nelbOLDOLD  30718  reuxfrdf  30740  inpr0  30781  ssiun3  30799  fmcncfil  31783  bnj115  32604  bnj946  32654  bnj1142  32669  bnj1211  32677  bnj1294  32697  bnj1385  32712  bnj110  32738  bnj611  32798  bnj864  32802  bnj865  32803  bnj1000  32821  bnj978  32829  bnj1049  32854  bnj1090  32859  bnj1133  32869  bnj1176  32885  bnj1186  32887  bnj1253  32897  bnj1388  32913  untuni  33550  fnssintima  33578  ralxp3f  33588  dfon2lem8  33672  frpoins3xpg  33714  frpoins3xp3g  33715  wzel  33745  eqscut2  33927  dfrdg4  34180  onsuct0  34557  bj-ralvw  34991  bj-rcleqf  35142  exrecfnlem  35477  fvineqsneq  35510  poimirlem25  35729  poimirlem30  35734  nninfnub  35836  mptbi12f  36251  pmapglbx  37710  cdlemefrs29bpre0  38337  sn-axrep5v  40113  dford4  40767  cllem0  41062  elmapintrab  41073  elintima  41150  ss2iundf  41156  ntrneiiso  41590  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  scottabf  41747  expandral  41797  ismnushort  41808  ralbidar  41952  rexbidar  41953  ssralv2  42040  en3lpVD  42354  ssralv2VD  42375  trintALTVD  42389  ssrabf  42553  rabssf  42557  dffo3f  42606  rexrsb  44479  nrhmzr  45319  empty-surprise  46372  alsconv  46380