Definition df-ral 2480

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

This definition is referenced by:  ralnex  2485  rexnalim  2486  dfrex2dc  2488  ralbida  2491  ralbidv2  2499  ralbid2  2501  ralbii2  2507  r2alf  2514  hbral  2526  hbra1  2527  nfra1  2528  nfraldw  2529  nfraldxy  2530  nfraldya  2532  r3al  2541  alral  2542  rsp  2544  rgen  2550  rgen2a  2551  ralim  2556  ralimi2  2557  ralimdaa  2563  ralimdv2  2567  ralrimi  2568  r19.21t  2572  ralrimd  2575  r19.21bi  2585  rexim  2591  r19.23t  2604  r19.26m  2628  r19.32r  2643  rabid2  2674  rabbi  2675  raleqf  2689  cbvralfw  2719  cbvralf  2721  cbvralvw  2733  cbvraldva2  2736  ralv  2780  ceqsralt  2790  rspct  2861  rspc  2862  rspcimdv  2869  rspc2gv  2880  ralab  2924  ralab2  2928  ralrab2  2929  reu2  2952  reu6  2953  reu3  2954  rmo4  2957  reu8  2960  rmo3f  2961  rmoim  2965  2reuswapdc  2968  2rmorex  2970  ra5  3078  rmo2ilem  3079  rmo3  3081  cbvralcsf  3147  dfss3  3173  dfss3f  3176  ssabral  3255  ss2rab  3260  rabss  3261  ssrab  3262  dfdif3  3274  ralunb  3345  reuss2  3444  rabeq0  3481  rabxmdc  3483  disj  3500  disj1  3502  r19.2m  3538  r19.2mOLD  3539  r19.3rm  3540  ralidm  3552  ralf0  3554  ralm  3555  ralsnsg  3660  ralsns  3661  unissb  3870  dfint2  3877  elint2  3882  elintrab  3887  ssintrab  3898  dfiin2g  3950  invdisj  4028  dftr5  4135  trint  4147  repizf2lem  4195  ordsucim  4537  ordunisuc2r  4551  setindel  4575  elirr  4578  en2lp  4591  zfregfr  4611  tfi  4619  zfinf2  4626  peano2  4632  peano5  4635  find  4636  raliunxp  4808  dmopab3  4880  issref  5053  asymref  5056  dffun7  5286  funcnv  5320  funcnvuni  5328  fnres  5377  fnopabg  5384  rexrnmpt  5708  dffo3  5712  acexmidlem2  5922  nfixpxy  6785  pw1dc0el  6981  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  fz1sbc  10188  nnwosdc  12231  isprm2  12310  istopg  14319  cbvrald  15518  decidr  15526  bdcint  15607  bdcriota  15613  bj-axempty  15623  bj-indind  15662  bj-ssom  15666  findset  15675  bj-nnord  15688  bj-inf2vn  15704  bj-inf2vn2  15705  bj-findis  15709  alsconv  15811