Definition df-ral 2516

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 2511	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2202	. . . 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  2521  rexnalim  2522  dfrex2dc  2524  ralbida  2527  ralbidv2  2535  ralbid2  2537  ralbii2  2543  r2alf  2550  hbral  2562  hbra1  2563  nfra1  2564  nfraldw  2565  nfraldxy  2566  nfraldya  2568  r3al  2577  alral  2578  rsp  2580  rgen  2586  rgen2a  2587  ralim  2592  ralimi2  2593  ralimdaa  2599  ralimdv2  2603  ralrimi  2604  r19.21t  2608  ralrimd  2611  r19.21bi  2621  rexim  2627  r19.23t  2641  r19.26m  2665  r19.32r  2680  rabid2  2711  rabbi  2712  raleqf  2727  cbvralfw  2757  cbvralf  2759  cbvralvw  2772  cbvraldva2  2775  ralv  2821  ceqsralt  2831  rspct  2904  rspc  2905  rspcimdv  2912  rspc2gv  2923  ralab  2967  ralab2  2971  ralrab2  2972  reu2  2995  reu6  2996  reu3  2997  rmo4  3000  reu8  3003  rmo3f  3004  rmoim  3008  2reuswapdc  3011  2rmorex  3013  ra5  3122  rmo2ilem  3123  rmo3  3125  cbvralcsf  3191  dfss3  3217  dfss3f  3220  ssabral  3299  ss2rab  3304  rabss  3305  ssrab  3306  dfdif3  3319  ralunb  3390  reuss2  3489  rabeq0  3526  rabxmdc  3528  disj  3545  disj1  3547  r19.2m  3583  r19.2mOLD  3584  r19.3rm  3585  ralidm  3597  ralf0  3599  ralm  3600  ralsnsg  3710  ralsns  3711  unissb  3928  dfint2  3935  elint2  3940  elintrab  3945  ssintrab  3956  dfiin2g  4008  invdisj  4086  dftr5  4195  trint  4207  repizf2lem  4257  ordsucim  4604  ordunisuc2r  4618  setindel  4642  elirr  4645  en2lp  4658  zfregfr  4678  tfi  4686  zfinf2  4693  peano2  4699  peano5  4702  find  4703  raliunxp  4877  dmopab3  4950  issref  5126  asymref  5129  dffun7  5360  funcnv  5398  funcnvuni  5406  fnres  5456  fnopabg  5463  rexrnmpt  5798  dffo3  5802  acexmidlem2  6025  nfixpxy  6929  pw1dc0el  7146  isomnimap  7396  ismkvmap  7413  iswomnimap  7425  fz1sbc  10393  nnwosdc  12690  isprm2  12769  istopg  14810  cbvrald  16506  decidr  16514  bdcint  16593  bdcriota  16599  bj-axempty  16609  bj-indind  16648  bj-ssom  16652  findset  16661  bj-nnord  16674  bj-inf2vn  16690  bj-inf2vn2  16691  bj-findis  16695  alsconv  16823