Definition df-ral 2527

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 2522	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2205	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1396	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 105	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2532  rexnalim  2533  dfrex2dc  2535  ralbida  2538  ralbidv2  2546  ralbid2  2548  ralbii2  2554  r2alf  2561  hbral  2573  hbra1  2574  nfra1  2575  nfraldw  2576  nfraldxy  2577  nfraldya  2579  r3al  2588  alral  2589  rsp  2591  rgen  2597  rgen2a  2598  ralim  2603  ralimi2  2604  ralimdaa  2610  ralimdv2  2614  ralrimi  2615  r19.21t  2619  ralrimd  2622  r19.21bi  2632  rexim  2638  r19.23t  2652  r19.26m  2676  r19.32r  2691  rabid2  2723  rabbi  2724  raleqf  2739  cbvralfw  2769  cbvralf  2771  cbvralvw  2784  cbvraldva2  2787  ralv  2833  ceqsralt  2843  rspct  2916  rspc  2917  rspcimdv  2924  rspc2gv  2936  ralab  2980  ralab2  2984  ralrab2  2985  reu2  3008  reu6  3009  reu3  3010  rmo4  3013  reu8  3016  rmo3f  3017  rmoim  3021  2reuswapdc  3024  2rmorex  3026  ra5  3135  rmo2ilem  3136  rmo3  3138  cbvralcsf  3204  dfss3  3230  dfss3f  3234  ssabral  3313  ss2rab  3318  rabss  3319  ssrab  3320  dfdif3  3333  ralunb  3404  reuss2  3505  rabeq0  3542  disj  3561  disj1  3563  r19.2m  3600  r19.2mOLD  3601  r19.3rm  3602  ralidm  3614  ralf0  3616  ralm  3617  ralsnsg  3731  ralsns  3732  unissb  3949  dfint2  3956  elint2  3961  elintrab  3966  ssintrab  3977  dfiin2g  4029  invdisj  4107  dftr5  4216  trint  4228  repizf2lem  4279  ordsucim  4627  ordunisuc2r  4641  setindel  4665  elirr  4668  en2lp  4681  zfregfr  4701  tfi  4709  zfinf2  4716  peano2  4722  peano5  4725  find  4726  raliunxp  4901  dmopab3  4974  issref  5150  asymref  5153  dffun7  5384  funcnv  5422  funcnvuni  5430  fnres  5480  fnopabg  5487  rexrnmpt  5825  dffo3  5829  acexmidlem2  6055  nfixpxy  6965  pw1dc0el  7184  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  fz1sbc  10452  nnwosdc  12760  isprm2  12839  istopg  14990  cbvrald  16686  decidr  16694  bdcint  16773  bdcriota  16779  bj-axempty  16789  bj-indind  16828  bj-ssom  16832  findset  16841  bj-nnord  16854  bj-inf2vn  16870  bj-inf2vn2  16871  bj-findis  16875  alsconv  16992