Definition df-ral 2375

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 2370	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1295	. . . . 5 class 𝑥
6	5, 3	wcel 1445	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1294	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 104	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2380  rexnalim  2381  dfrex2dc  2382  ralbida  2385  ralbidv2  2393  ralbii2  2399  r2alf  2406  hbral  2418  hbra1  2419  nfra1  2420  nfraldxy  2421  nfraldya  2423  r3al  2431  alral  2432  rsp  2434  rgen  2439  rgen2a  2440  ralim  2445  ralimi2  2446  ralimdaa  2452  ralimdv2  2455  ralrimi  2456  r19.21t  2460  ralrimd  2463  r19.21bi  2473  rexim  2479  r19.23t  2492  r19.26m  2514  r19.32r  2528  rabid2  2557  rabbi  2558  raleqf  2572  cbvralf  2598  cbvraldva2  2608  ralv  2650  ceqsralt  2660  rspct  2729  rspc  2730  rspcimdv  2737  rspc2gv  2747  ralab  2789  ralab2  2793  ralrab2  2794  reu2  2817  reu6  2818  reu3  2819  rmo4  2822  reu8  2825  rmo3f  2826  rmoim  2830  2reuswapdc  2833  2rmorex  2835  ra5  2941  rmo2ilem  2942  rmo3  2944  cbvralcsf  3004  dfss3  3029  dfss3f  3031  ssabral  3107  ss2rab  3112  rabss  3113  ssrab  3114  dfdif3  3125  ralunb  3196  reuss2  3295  rabeq0  3331  rabxmdc  3333  disj  3350  disj1  3352  r19.2m  3388  r19.2mOLD  3389  r19.3rm  3390  ralidm  3402  rgenm  3404  ralf0  3405  ralm  3406  ralsnsg  3500  ralsns  3501  unissb  3705  dfint2  3712  elint2  3717  elintrab  3722  ssintrab  3733  dfiin2g  3785  invdisj  3861  dftr5  3961  trint  3973  repizf2lem  4017  ordsucim  4345  ordunisuc2r  4359  setindel  4382  elirr  4385  en2lp  4398  zfregfr  4417  tfi  4425  zfinf2  4432  peano2  4438  peano5  4441  find  4442  raliunxp  4608  dmopab3  4680  issref  4847  asymref  4850  dffun7  5076  funcnv  5109  funcnvuni  5117  fnres  5164  fnopabg  5171  rexrnmpt  5481  dffo3  5485  acexmidlem2  5687  nfixpxy  6514  isomnimap  6880  ismkvmap  6898  fz1sbc  9659  isprm2  11526  istopg  11850  cbvrald  12396  decidr  12404  bdcint  12476  bdcriota  12482  bj-axempty  12492  bj-indind  12535  bj-ssom  12539  findset  12548  bj-nnord  12561  bj-inf2vn  12577  bj-inf2vn2  12578  bj-findis  12582  alsconv  12628