Definition df-ral 2453

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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wral 2448	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1347	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1346	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 104	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2458  rexnalim  2459  dfrex2dc  2461  ralbida  2464  ralbidv2  2472  ralbid2  2474  ralbii2  2480  r2alf  2487  hbral  2499  hbra1  2500  nfra1  2501  nfraldw  2502  nfraldxy  2503  nfraldya  2505  r3al  2514  alral  2515  rsp  2517  rgen  2523  rgen2a  2524  ralim  2529  ralimi2  2530  ralimdaa  2536  ralimdv2  2540  ralrimi  2541  r19.21t  2545  ralrimd  2548  r19.21bi  2558  rexim  2564  r19.23t  2577  r19.26m  2601  r19.32r  2616  rabid2  2646  rabbi  2647  raleqf  2661  cbvralfw  2687  cbvralf  2689  cbvralvw  2700  cbvraldva2  2703  ralv  2747  ceqsralt  2757  rspct  2827  rspc  2828  rspcimdv  2835  rspc2gv  2846  ralab  2890  ralab2  2894  ralrab2  2895  reu2  2918  reu6  2919  reu3  2920  rmo4  2923  reu8  2926  rmo3f  2927  rmoim  2931  2reuswapdc  2934  2rmorex  2936  ra5  3043  rmo2ilem  3044  rmo3  3046  cbvralcsf  3111  dfss3  3137  dfss3f  3139  ssabral  3218  ss2rab  3223  rabss  3224  ssrab  3225  dfdif3  3237  ralunb  3308  reuss2  3407  rabeq0  3443  rabxmdc  3445  disj  3462  disj1  3464  r19.2m  3500  r19.2mOLD  3501  r19.3rm  3502  ralidm  3514  rgenm  3516  ralf0  3517  ralm  3518  ralsnsg  3618  ralsns  3619  unissb  3824  dfint2  3831  elint2  3836  elintrab  3841  ssintrab  3852  dfiin2g  3904  invdisj  3981  dftr5  4088  trint  4100  repizf2lem  4145  ordsucim  4482  ordunisuc2r  4496  setindel  4520  elirr  4523  en2lp  4536  zfregfr  4556  tfi  4564  zfinf2  4571  peano2  4577  peano5  4580  find  4581  raliunxp  4750  dmopab3  4822  issref  4991  asymref  4994  dffun7  5223  funcnv  5257  funcnvuni  5265  fnres  5312  fnopabg  5319  rexrnmpt  5636  dffo3  5640  acexmidlem2  5847  nfixpxy  6691  pw1dc0el  6885  isomnimap  7109  ismkvmap  7126  iswomnimap  7138  fz1sbc  10039  nnwosdc  11981  isprm2  12058  istopg  12750  cbvrald  13782  decidr  13790  bdcint  13872  bdcriota  13878  bj-axempty  13888  bj-indind  13927  bj-ssom  13931  findset  13940  bj-nnord  13953  bj-inf2vn  13969  bj-inf2vn2  13970  bj-findis  13974  alsconv  14069